diff --git a/src/Doc/Implementation/Local_Theory.thy b/src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy +++ b/src/Doc/Implementation/Local_Theory.thy @@ -1,149 +1,149 @@ (*:maxLineLen=78:*) theory Local_Theory imports Base begin chapter \Local theory specifications \label{ch:local-theory}\ text \ A \<^emph>\local theory\ combines aspects of both theory and proof context (cf.\ \secref{sec:context}), such that definitional specifications may be given relatively to parameters and assumptions. A local theory is represented as a regular proof context, augmented by administrative data about the \<^emph>\target context\. The target is usually derived from the background theory by adding local \\\ and \\\ elements, plus suitable modifications of non-logical context data (e.g.\ a special type-checking discipline). Once initialized, the target is ready to absorb definitional primitives: \\\ for terms and \\\ for theorems. Such definitions may get transformed in a target-specific way, but the programming interface hides such details. Isabelle/Pure provides target mechanisms for locales, type-classes, type-class instantiations, and general overloading. In principle, users can implement new targets as well, but this rather arcane discipline is beyond the scope of this manual. In contrast, implementing derived definitional packages to be used within a local theory context is quite easy: the interfaces are even simpler and more abstract than the underlying primitives for raw theories. Many definitional packages for local theories are available in Isabelle. Although a few old packages only work for global theories, the standard way of implementing definitional packages in Isabelle is via the local theory interface. \ section \Definitional elements\ text \ There are separate elements \\ c \ t\ for terms, and \\ b = thm\ for theorems. Types are treated implicitly, according to Hindley-Milner discipline (cf.\ \secref{sec:variables}). These definitional primitives essentially act like \let\-bindings within a local context that may already contain earlier \let\-bindings and some initial \\\-bindings. Thus we gain \<^emph>\dependent definitions\ that are relative to an initial axiomatic context. The following diagram illustrates this idea of axiomatic elements versus definitional elements: \begin{center} \begin{tabular}{|l|l|l|} \hline & \\\-binding & \let\-binding \\ \hline types & fixed \\\ & arbitrary \\\ \\ terms & \\ x :: \\ & \\ c \ t\ \\ theorems & \\ a: A\ & \\ b = \<^BG>B\<^EN>\ \\ \hline \end{tabular} \end{center} A user package merely needs to produce suitable \\\ and \\\ elements according to the application. For example, a package for inductive definitions might first \\\ a certain predicate as some fixed-point construction, then \\\ a proven result about monotonicity of the functor involved here, and then produce further derived concepts via additional \\\ and \\\ elements. The cumulative sequence of \\\ and \\\ produced at package runtime is managed by the local theory infrastructure by means of an \<^emph>\auxiliary context\. Thus the system holds up the impression of working within a fully abstract situation with hypothetical entities: \\ c \ t\ always results in a literal fact \\<^BG>c \ t\<^EN>\, where \c\ is a fixed variable \c\. The details about global constants, name spaces etc. are handled internally. So the general structure of a local theory is a sandwich of three layers: \begin{center} \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}} \end{center} When a definitional package is finished, the auxiliary context is reset to the target context. The target now holds definitions for terms and theorems that stem from the hypothetical \\\ and \\\ elements, transformed by the particular target policy (see @{cite \\S4--5\ "Haftmann-Wenzel:2009"} for details). \ text %mlref \ \begin{mldecls} @{index_ML_type local_theory: Proof.context} \\ - @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] + @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory"} \\ @{index_ML Local_Theory.note: "Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\local_theory\ represents local theories. Although this is merely an alias for \<^ML_type>\Proof.context\, it is semantically a subtype of the same: a \<^ML_type>\local_theory\ holds target information as special context data. Subtyping means that any value \lthy:\~\<^ML_type>\local_theory\ can be also used with operations on expecting a regular \ctxt:\~\<^ML_type>\Proof.context\. - \<^descr> \<^ML>\Named_Target.init\~\before_exit name thy\ initializes a local theory + \<^descr> \<^ML>\Named_Target.init\~\includes name thy\ initializes a local theory derived from the given background theory. An empty name refers to a \<^emph>\global theory\ context, and a non-empty name refers to a @{command locale} or @{command class} context (a fully-qualified internal name is expected here). This is useful for experimentation --- normally the Isar toplevel already takes care to initialize the local theory context. \<^descr> \<^ML>\Local_Theory.define\~\((b, mx), (a, rhs)) lthy\ defines a local entity according to the specification that is given relatively to the current \lthy\ context. In particular the term of the RHS may refer to earlier local entities from the auxiliary context, or hypothetical parameters from the target context. The result is the newly defined term (which is always a fixed variable with exactly the same name as specified for the LHS), together with an equational theorem that states the definition as a hypothetical fact. Unless an explicit name binding is given for the RHS, the resulting fact will be called \b_def\. Any given attributes are applied to that same fact --- immediately in the auxiliary context \<^emph>\and\ in any transformed versions stemming from target-specific policies or any later interpretations of results from the target context (think of @{command locale} and @{command interpretation}, for example). This means that attributes should be usually plain declarations such as @{attribute simp}, while non-trivial rules like @{attribute simplified} are better avoided. \<^descr> \<^ML>\Local_Theory.note\~\(a, ths) lthy\ is analogous to \<^ML>\Local_Theory.define\, but defines facts instead of terms. There is also a slightly more general variant \<^ML>\Local_Theory.notes\ that defines several facts (with attribute expressions) simultaneously. This is essentially the internal version of the @{command lemmas} command, or @{command declare} if an empty name binding is given. \ section \Morphisms and declarations \label{sec:morphisms}\ text \ %FIXME See also @{cite "Chaieb-Wenzel:2007"}. \ end diff --git a/src/HOL/Library/Perm.thy b/src/HOL/Library/Perm.thy --- a/src/HOL/Library/Perm.thy +++ b/src/HOL/Library/Perm.thy @@ -1,810 +1,810 @@ (* Author: Florian Haftmann, TU Muenchen *) section \Permutations as abstract type\ theory Perm imports Main begin text \ This theory introduces basics about permutations, i.e. almost everywhere fix bijections. But it is by no means complete. Grieviously missing are cycles since these would require more elaboration, e.g. the concept of distinct lists equivalent under rotation, which maybe would also deserve its own theory. But see theory \src/HOL/ex/Perm_Fragments.thy\ for fragments on that. \ subsection \Abstract type of permutations\ typedef 'a perm = "{f :: 'a \ 'a. bij f \ finite {a. f a \ a}}" morphisms "apply" Perm proof show "id \ ?perm" by simp qed setup_lifting type_definition_perm notation "apply" (infixl "\$\" 999) lemma bij_apply [simp]: "bij (apply f)" using "apply" [of f] by simp lemma perm_eqI: assumes "\a. f \$\ a = g \$\ a" shows "f = g" using assms by transfer (simp add: fun_eq_iff) lemma perm_eq_iff: "f = g \ (\a. f \$\ a = g \$\ a)" by (auto intro: perm_eqI) lemma apply_inj: "f \$\ a = f \$\ b \ a = b" by (rule inj_eq) (rule bij_is_inj, simp) lift_definition affected :: "'a perm \ 'a set" is "\f. {a. f a \ a}" . lemma in_affected: "a \ affected f \ f \$\ a \ a" by transfer simp lemma finite_affected [simp]: "finite (affected f)" by transfer simp lemma apply_affected [simp]: "f \$\ a \ affected f \ a \ affected f" proof transfer fix f :: "'a \ 'a" and a :: 'a assume "bij f \ finite {b. f b \ b}" then have "bij f" by simp interpret bijection f by standard (rule \bij f\) have "f a \ {a. f a = a} \ a \ {a. f a = a}" (is "?P \ ?Q") by auto then show "f a \ {a. f a \ a} \ a \ {a. f a \ a}" by simp qed lemma card_affected_not_one: "card (affected f) \ 1" proof interpret bijection "apply f" by standard (rule bij_apply) assume "card (affected f) = 1" then obtain a where *: "affected f = {a}" by (rule card_1_singletonE) then have **: "f \$\ a \ a" by (simp flip: in_affected) with * have "f \$\ a \ affected f" by simp then have "f \$\ (f \$\ a) = f \$\ a" by (simp add: in_affected) then have "inv (apply f) (f \$\ (f \$\ a)) = inv (apply f) (f \$\ a)" by simp with ** show False by simp qed subsection \Identity, composition and inversion\ instantiation Perm.perm :: (type) "{monoid_mult, inverse}" begin lift_definition one_perm :: "'a perm" is id by simp lemma apply_one [simp]: "apply 1 = id" by (fact one_perm.rep_eq) lemma affected_one [simp]: "affected 1 = {}" by transfer simp lemma affected_empty_iff [simp]: "affected f = {} \ f = 1" by transfer auto lift_definition times_perm :: "'a perm \ 'a perm \ 'a perm" is comp proof fix f g :: "'a \ 'a" assume "bij f \ finite {a. f a \ a}" "bij g \finite {a. g a \ a}" then have "finite ({a. f a \ a} \ {a. g a \ a})" by simp moreover have "{a. (f \ g) a \ a} \ {a. f a \ a} \ {a. g a \ a}" by auto ultimately show "finite {a. (f \ g) a \ a}" by (auto intro: finite_subset) qed (auto intro: bij_comp) lemma apply_times: "apply (f * g) = apply f \ apply g" by (fact times_perm.rep_eq) lemma apply_sequence: "f \$\ (g \$\ a) = apply (f * g) a" by (simp add: apply_times) lemma affected_times [simp]: "affected (f * g) \ affected f \ affected g" by transfer auto lift_definition inverse_perm :: "'a perm \ 'a perm" is inv proof transfer fix f :: "'a \ 'a" and a assume "bij f \ finite {b. f b \ b}" then have "bij f" and fin: "finite {b. f b \ b}" by auto interpret bijection f by standard (rule \bij f\) from fin show "bij (inv f) \ finite {a. inv f a \ a}" by (simp add: bij_inv) qed instance by standard (transfer; simp add: comp_assoc)+ end lemma apply_inverse: "apply (inverse f) = inv (apply f)" by (fact inverse_perm.rep_eq) lemma affected_inverse [simp]: "affected (inverse f) = affected f" proof transfer fix f :: "'a \ 'a" and a assume "bij f \ finite {b. f b \ b}" then have "bij f" by simp interpret bijection f by standard (rule \bij f\) show "{a. inv f a \ a} = {a. f a \ a}" by simp qed global_interpretation perm: group times "1::'a perm" inverse proof fix f :: "'a perm" show "1 * f = f" by transfer simp show "inverse f * f = 1" proof transfer fix f :: "'a \ 'a" and a assume "bij f \ finite {b. f b \ b}" then have "bij f" by simp interpret bijection f by standard (rule \bij f\) show "inv f \ f = id" by simp qed qed declare perm.inverse_distrib_swap [simp] lemma perm_mult_commute: assumes "affected f \ affected g = {}" shows "g * f = f * g" proof (rule perm_eqI) fix a from assms have *: "a \ affected f \ a \ affected g" "a \ affected g \ a \ affected f" for a by auto consider "a \ affected f \ a \ affected g \ f \$\ a \ affected f" | "a \ affected f \ a \ affected g \ f \$\ a \ affected f" | "a \ affected f \ a \ affected g" using assms by auto then show "(g * f) \$\ a = (f * g) \$\ a" proof cases case 1 with * have "f \$\ a \ affected g" by auto with 1 show ?thesis by (simp add: in_affected apply_times) next case 2 with * have "g \$\ a \ affected f" by auto with 2 show ?thesis by (simp add: in_affected apply_times) next case 3 then show ?thesis by (simp add: in_affected apply_times) qed qed lemma apply_power: "apply (f ^ n) = apply f ^^ n" by (induct n) (simp_all add: apply_times) lemma perm_power_inverse: "inverse f ^ n = inverse ((f :: 'a perm) ^ n)" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case unfolding power_Suc2 [of f] by simp qed subsection \Orbit and order of elements\ definition orbit :: "'a perm \ 'a \ 'a set" where "orbit f a = range (\n. (f ^ n) \$\ a)" lemma in_orbitI: assumes "(f ^ n) \$\ a = b" shows "b \ orbit f a" using assms by (auto simp add: orbit_def) lemma apply_power_self_in_orbit [simp]: "(f ^ n) \$\ a \ orbit f a" by (rule in_orbitI) rule lemma in_orbit_self [simp]: "a \ orbit f a" using apply_power_self_in_orbit [of _ 0] by simp lemma apply_self_in_orbit [simp]: "f \$\ a \ orbit f a" using apply_power_self_in_orbit [of _ 1] by simp lemma orbit_not_empty [simp]: "orbit f a \ {}" using in_orbit_self [of a f] by blast lemma not_in_affected_iff_orbit_eq_singleton: "a \ affected f \ orbit f a = {a}" (is "?P \ ?Q") proof assume ?P then have "f \$\ a = a" by (simp add: in_affected) then have "(f ^ n) \$\ a = a" for n by (induct n) (simp_all add: apply_times) then show ?Q by (auto simp add: orbit_def) next assume ?Q then show ?P by (auto simp add: orbit_def in_affected dest: range_eq_singletonD [of _ _ 1]) qed definition order :: "'a perm \ 'a \ nat" where "order f = card \ orbit f" lemma orbit_subset_eq_affected: assumes "a \ affected f" shows "orbit f a \ affected f" proof (rule ccontr) assume "\ orbit f a \ affected f" then obtain b where "b \ orbit f a" and "b \ affected f" by auto then have "b \ range (\n. (f ^ n) \$\ a)" by (simp add: orbit_def) then obtain n where "b = (f ^ n) \$\ a" by blast with \b \ affected f\ have "(f ^ n) \$\ a \ affected f" by simp then have "f \$\ a \ affected f" by (induct n) (simp_all add: apply_times) with assms show False by simp qed lemma finite_orbit [simp]: "finite (orbit f a)" proof (cases "a \ affected f") case False then show ?thesis by (simp add: not_in_affected_iff_orbit_eq_singleton) next case True then have "orbit f a \ affected f" by (rule orbit_subset_eq_affected) then show ?thesis using finite_affected by (rule finite_subset) qed lemma orbit_1 [simp]: "orbit 1 a = {a}" by (auto simp add: orbit_def) lemma order_1 [simp]: "order 1 a = 1" unfolding order_def by simp lemma card_orbit_eq [simp]: "card (orbit f a) = order f a" by (simp add: order_def) lemma order_greater_zero [simp]: "order f a > 0" by (simp only: card_gt_0_iff order_def comp_def) simp lemma order_eq_one_iff: "order f a = Suc 0 \ a \ affected f" (is "?P \ ?Q") proof assume ?P then have "card (orbit f a) = 1" by simp then obtain b where "orbit f a = {b}" by (rule card_1_singletonE) with in_orbit_self [of a f] have "b = a" by simp with \orbit f a = {b}\ show ?Q by (simp add: not_in_affected_iff_orbit_eq_singleton) next assume ?Q then have "orbit f a = {a}" by (simp add: not_in_affected_iff_orbit_eq_singleton) then have "card (orbit f a) = 1" by simp then show ?P by simp qed lemma order_greater_eq_two_iff: "order f a \ 2 \ a \ affected f" using order_eq_one_iff [of f a] apply (auto simp add: neq_iff) using order_greater_zero [of f a] apply simp done lemma order_less_eq_affected: assumes "f \ 1" shows "order f a \ card (affected f)" proof (cases "a \ affected f") from assms have "affected f \ {}" by simp then obtain B b where "affected f = insert b B" by blast with finite_affected [of f] have "card (affected f) \ 1" by (simp add: card.insert_remove) case False then have "order f a = 1" by (simp add: order_eq_one_iff) with \card (affected f) \ 1\ show ?thesis by simp next case True have "card (orbit f a) \ card (affected f)" by (rule card_mono) (simp_all add: True orbit_subset_eq_affected card_mono) then show ?thesis by simp qed lemma affected_order_greater_eq_two: assumes "a \ affected f" shows "order f a \ 2" proof (rule ccontr) assume "\ 2 \ order f a" then have "order f a < 2" by (simp add: not_le) with order_greater_zero [of f a] have "order f a = 1" by arith with assms show False by (simp add: order_eq_one_iff) qed lemma order_witness_unfold: assumes "n > 0" and "(f ^ n) \$\ a = a" shows "order f a = card ((\m. (f ^ m) \$\ a) ` {0..m. (f ^ m) \$\ a) ` {0.. orbit f a" then obtain m where "(f ^ m) \$\ a = b" by (auto simp add: orbit_def) then have "b = (f ^ (m mod n + n * (m div n))) \$\ a" by simp also have "\ = (f ^ (m mod n)) \$\ ((f ^ (n * (m div n))) \$\ a)" by (simp only: power_add apply_times) simp also have "(f ^ (n * q)) \$\ a = a" for q by (induct q) (simp_all add: power_add apply_times assms) finally have "b = (f ^ (m mod n)) \$\ a" . moreover from \n > 0\ have "m mod n < n" by simp ultimately show "b \ ?B" by auto next fix b assume "b \ ?B" then obtain m where "(f ^ m) \$\ a = b" by blast then show "b \ orbit f a" by (rule in_orbitI) qed then have "card (orbit f a) = card ?B" by (simp only:) then show ?thesis by simp qed lemma inj_on_apply_range: "inj_on (\m. (f ^ m) \$\ a) {..m. (f ^ m) \$\ a) {.. order f a" for n using that proof (induct n) case 0 then show ?case by simp next case (Suc n) then have prem: "n < order f a" by simp with Suc.hyps have hyp: "inj_on (\m. (f ^ m) \$\ a) {..$\ a \ (\m. (f ^ m) \$\ a) ` {..$\ a \ (\m. (f ^ m) \$\ a) ` {..$\ a = (f ^ n) \$\ a" and "m < n" by auto interpret bijection "apply (f ^ m)" by standard simp from \m < n\ have "n = m + (n - m)" and nm: "0 < n - m" "n - m \ n" by arith+ with * have "(f ^ m) \$\ a = (f ^ (m + (n - m))) \$\ a" by simp then have "(f ^ m) \$\ a = (f ^ m) \$\ ((f ^ (n - m)) \$\ a)" by (simp add: power_add apply_times) then have "(f ^ (n - m)) \$\ a = a" by simp with \n - m > 0\ have "order f a = card ((\m. (f ^ m) \$\ a) ` {0..m. (f ^ m) \$\ a) ` {0.. card {0.. n - m" by simp with prem show False by simp qed with hyp show ?case by (simp add: lessThan_Suc) qed then show ?thesis by simp qed lemma orbit_unfold_image: "orbit f a = (\n. (f ^ n) \$\ a) ` {.. orbit f a" by (auto simp add: orbit_def) from inj_on_apply_range [of f a] have "card ?A = order f a" by (auto simp add: card_image) then show "card ?A = card (orbit f a)" by simp qed lemma in_orbitE: assumes "b \ orbit f a" obtains n where "b = (f ^ n) \$\ a" and "n < order f a" using assms unfolding orbit_unfold_image by blast lemma apply_power_order [simp]: "(f ^ order f a) \$\ a = a" proof - have "(f ^ order f a) \$\ a \ orbit f a" by simp then obtain n where *: "(f ^ order f a) \$\ a = (f ^ n) \$\ a" and "n < order f a" by (rule in_orbitE) show ?thesis proof (cases n) case 0 with * show ?thesis by simp next case (Suc m) from order_greater_zero [of f a] have "Suc (order f a - 1) = order f a" by arith from Suc \n < order f a\ have "m < order f a" by simp with Suc * have "(inverse f) \$\ ((f ^ Suc (order f a - 1)) \$\ a) = (inverse f) \$\ ((f ^ Suc m) \$\ a)" by simp then have "(f ^ (order f a - 1)) \$\ a = (f ^ m) \$\ a" by (simp only: power_Suc apply_times) (simp add: apply_sequence mult.assoc [symmetric]) with inj_on_apply_range have "order f a - 1 = m" by (rule inj_onD) (simp_all add: \m < order f a\) with Suc have "n = order f a" by auto with \n < order f a\ show ?thesis by simp qed qed lemma apply_power_left_mult_order [simp]: "(f ^ (n * order f a)) \$\ a = a" by (induct n) (simp_all add: power_add apply_times) lemma apply_power_right_mult_order [simp]: "(f ^ (order f a * n)) \$\ a = a" by (simp add: ac_simps) lemma apply_power_mod_order_eq [simp]: "(f ^ (n mod order f a)) \$\ a = (f ^ n) \$\ a" proof - have "(f ^ n) \$\ a = (f ^ (n mod order f a + order f a * (n div order f a))) \$\ a" by simp also have "\ = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \$\ a" by (simp flip: power_add) finally show ?thesis by (simp add: apply_times) qed lemma apply_power_eq_iff: "(f ^ m) \$\ a = (f ^ n) \$\ a \ m mod order f a = n mod order f a" (is "?P \ ?Q") proof assume ?Q then have "(f ^ (m mod order f a)) \$\ a = (f ^ (n mod order f a)) \$\ a" by simp then show ?P by simp next assume ?P then have "(f ^ (m mod order f a)) \$\ a = (f ^ (n mod order f a)) \$\ a" by simp with inj_on_apply_range show ?Q by (rule inj_onD) simp_all qed lemma apply_inverse_eq_apply_power_order_minus_one: "(inverse f) \$\ a = (f ^ (order f a - 1)) \$\ a" proof (cases "order f a") case 0 with order_greater_zero [of f a] show ?thesis by simp next case (Suc n) moreover have "(f ^ order f a) \$\ a = a" by simp then have *: "(inverse f) \$\ ((f ^ order f a) \$\ a) = (inverse f) \$\ a" by simp ultimately show ?thesis by (simp add: apply_sequence mult.assoc [symmetric]) qed lemma apply_inverse_self_in_orbit [simp]: "(inverse f) \$\ a \ orbit f a" using apply_inverse_eq_apply_power_order_minus_one [symmetric] by (rule in_orbitI) lemma apply_inverse_power_eq: "(inverse (f ^ n)) \$\ a = (f ^ (order f a - n mod order f a)) \$\ a" proof (induct n) case 0 then show ?case by simp next case (Suc n) define m where "m = order f a - n mod order f a - 1" moreover have "order f a - n mod order f a > 0" by simp ultimately have *: "order f a - n mod order f a = Suc m" by arith moreover from * have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)" by (auto simp add: mod_Suc) ultimately show ?case using Suc by (simp_all add: apply_times power_Suc2 [of _ n] power_Suc [of _ m] del: power_Suc) (simp add: apply_sequence mult.assoc [symmetric]) qed lemma apply_power_eq_self_iff: "(f ^ n) \$\ a = a \ order f a dvd n" using apply_power_eq_iff [of f n a 0] by (simp add: mod_eq_0_iff_dvd) lemma orbit_equiv: assumes "b \ orbit f a" shows "orbit f b = orbit f a" (is "?B = ?A") proof from assms obtain n where "n < order f a" and b: "b = (f ^ n) \$\ a" by (rule in_orbitE) then show "?B \ ?A" by (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) from b have "(inverse (f ^ n)) \$\ b = (inverse (f ^ n)) \$\ ((f ^ n) \$\ a)" by simp then have a: "a = (inverse (f ^ n)) \$\ b" by (simp add: apply_sequence) then show "?A \ ?B" apply (auto simp add: apply_sequence power_add [symmetric] intro: in_orbitI elim!: in_orbitE) unfolding apply_times comp_def apply_inverse_power_eq unfolding apply_sequence power_add [symmetric] apply (rule in_orbitI) apply rule done qed lemma orbit_apply [simp]: "orbit f (f \$\ a) = orbit f a" by (rule orbit_equiv) simp lemma order_apply [simp]: "order f (f \$\ a) = order f a" by (simp only: order_def comp_def orbit_apply) lemma orbit_apply_inverse [simp]: "orbit f (inverse f \$\ a) = orbit f a" by (rule orbit_equiv) simp lemma order_apply_inverse [simp]: "order f (inverse f \$\ a) = order f a" by (simp only: order_def comp_def orbit_apply_inverse) lemma orbit_apply_power [simp]: "orbit f ((f ^ n) \$\ a) = orbit f a" by (rule orbit_equiv) simp lemma order_apply_power [simp]: "order f ((f ^ n) \$\ a) = order f a" by (simp only: order_def comp_def orbit_apply_power) lemma orbit_inverse [simp]: "orbit (inverse f) = orbit f" proof (rule ext, rule set_eqI, rule) fix b a assume "b \ orbit f a" then obtain n where b: "b = (f ^ n) \$\ a" "n < order f a" by (rule in_orbitE) then have "b = apply (inverse (inverse f) ^ n) a" by simp then have "b = apply (inverse (inverse f ^ n)) a" by (simp add: perm_power_inverse) then have "b = apply (inverse f ^ (n * (order (inverse f ^ n) a - 1))) a" by (simp add: apply_inverse_eq_apply_power_order_minus_one power_mult) then show "b \ orbit (inverse f) a" by simp next fix b a assume "b \ orbit (inverse f) a" then show "b \ orbit f a" by (rule in_orbitE) (simp add: apply_inverse_eq_apply_power_order_minus_one perm_power_inverse power_mult [symmetric]) qed lemma order_inverse [simp]: "order (inverse f) = order f" by (simp add: order_def) lemma orbit_disjoint: assumes "orbit f a \ orbit f b" shows "orbit f a \ orbit f b = {}" proof (rule ccontr) assume "orbit f a \ orbit f b \ {}" then obtain c where "c \ orbit f a \ orbit f b" by blast then have "c \ orbit f a" and "c \ orbit f b" by auto then obtain m n where "c = (f ^ m) \$\ a" and "c = apply (f ^ n) b" by (blast elim!: in_orbitE) then have "(f ^ m) \$\ a = apply (f ^ n) b" by simp then have "apply (inverse f ^ m) ((f ^ m) \$\ a) = apply (inverse f ^ m) (apply (f ^ n) b)" by simp then have *: "apply (inverse f ^ m * f ^ n) b = a" by (simp add: apply_sequence perm_power_inverse) have "a \ orbit f b" proof (cases n m rule: linorder_cases) case equal with * show ?thesis by (simp add: perm_power_inverse) next case less moreover define q where "q = m - n" ultimately have "m = q + n" by arith with * have "apply (inverse f ^ q) b = a" by (simp add: power_add mult.assoc perm_power_inverse) then have "a \ orbit (inverse f) b" by (rule in_orbitI) then show ?thesis by simp next case greater moreover define q where "q = n - m" ultimately have "n = m + q" by arith with * have "apply (f ^ q) b = a" by (simp add: power_add mult.assoc [symmetric] perm_power_inverse) then show ?thesis by (rule in_orbitI) qed with assms show False by (auto dest: orbit_equiv) qed subsection \Swaps\ -lift_definition swap :: "'a \ 'a \ 'a perm" ("\_\_\") +lift_definition swap :: "'a \ 'a \ 'a perm" ("\_ \ _\") is "\a b. Fun.swap a b id" proof fix a b :: 'a have "{c. Fun.swap a b id c \ c} \ {a, b}" by (auto simp add: Fun.swap_def) then show "finite {c. Fun.swap a b id c \ c}" by (rule finite_subset) simp qed simp lemma apply_swap_simp [simp]: - "\a\b\ \$\ a = b" - "\a\b\ \$\ b = a" + "\a \ b\ \$\ a = b" + "\a \ b\ \$\ b = a" by (transfer; simp)+ lemma apply_swap_same [simp]: - "c \ a \ c \ b \ \a\b\ \$\ c = c" + "c \ a \ c \ b \ \a \ b\ \$\ c = c" by transfer simp lemma apply_swap_eq_iff [simp]: - "\a\b\ \$\ c = a \ c = b" - "\a\b\ \$\ c = b \ c = a" + "\a \ b\ \$\ c = a \ c = b" + "\a \ b\ \$\ c = b \ c = a" by (transfer; auto simp add: Fun.swap_def)+ lemma swap_1 [simp]: - "\a\a\ = 1" + "\a \ a\ = 1" by transfer simp lemma swap_sym: - "\b\a\ = \a\b\" + "\b \ a\ = \a \ b\" by (transfer; auto simp add: Fun.swap_def)+ lemma swap_self [simp]: - "\a\b\ * \a\b\ = 1" + "\a \ b\ * \a \ b\ = 1" by transfer (simp add: Fun.swap_def fun_eq_iff) lemma affected_swap: - "a \ b \ affected \a\b\ = {a, b}" + "a \ b \ affected \a \ b\ = {a, b}" by transfer (auto simp add: Fun.swap_def) lemma inverse_swap [simp]: - "inverse \a\b\ = \a\b\" + "inverse \a \ b\ = \a \ b\" by transfer (auto intro: inv_equality simp: Fun.swap_def) subsection \Permutations specified by cycles\ fun cycle :: "'a list \ 'a perm" ("\_\") where "\[]\ = 1" | "\[a]\ = 1" | "\a # b # as\ = \a # as\ * \a\b\" text \ We do not continue and restrict ourselves to syntax from here. See also introductory note. \ subsection \Syntax\ bundle no_permutation_syntax begin - no_notation swap ("\_\_\") + no_notation swap ("\_ \ _\") no_notation cycle ("\_\") no_notation "apply" (infixl "\$\" 999) end bundle permutation_syntax begin - notation swap ("\_\_\") + notation swap ("\_ \ _\") notation cycle ("\_\") notation "apply" (infixl "\$\" 999) end unbundle no_permutation_syntax end diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1166 +1,1167 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Library" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Leftist_Heap Binomial_Heap document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Hoare document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples + Specifications_with_bundle_mixins Sqrt Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid LDL TLList Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle" in Mirabelle = HOL + theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + options [timeout = 60] theories Ex session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Tests SMT_Tests_Verit SMT_Examples_Verit session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Mueller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Mueller The Alternating Bit Protocol performed in I/O-Automata. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Mueller. " theories Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Mueller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Mueller " theories TrivEx TrivEx2 diff --git a/src/HOL/Statespace/state_space.ML b/src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML +++ b/src/HOL/Statespace/state_space.ML @@ -1,663 +1,663 @@ (* Title: HOL/Statespace/state_space.ML Author: Norbert Schirmer, TU Muenchen *) signature STATE_SPACE = sig val distinct_compsN : string val getN : string val putN : string val injectN : string val namespaceN : string val projectN : string val valuetypesN : string val namespace_definition : bstring -> typ -> (xstring, string) Expression.expr * (binding * string option * mixfix) list -> string list -> string list -> theory -> theory val define_statespace : string list -> string -> ((string * bool) * (string list * bstring * (string * string) list)) list -> (string * string) list -> theory -> theory val define_statespace_i : string option -> string list -> string -> ((string * bool) * (typ list * bstring * (string * string) list)) list -> (string * typ) list -> theory -> theory val statespace_decl : ((string list * bstring) * (((string * bool) * (string list * xstring * (bstring * bstring) list)) list * (bstring * string) list)) parser val neq_x_y : Proof.context -> term -> term -> thm option val distinctNameSolver : Simplifier.solver val distinctTree_tac : Proof.context -> int -> tactic val distinct_simproc : Simplifier.simproc val get_comp : Context.generic -> string -> (typ * string) option val get_silent : Context.generic -> bool val set_silent : bool -> Context.generic -> Context.generic val gen_lookup_tr : Proof.context -> term -> string -> term val lookup_swap_tr : Proof.context -> term list -> term val lookup_tr : Proof.context -> term list -> term val lookup_tr' : Proof.context -> term list -> term val gen_update_tr : bool -> Proof.context -> string -> term -> term -> term val update_tr : Proof.context -> term list -> term val update_tr' : Proof.context -> term list -> term end; structure StateSpace : STATE_SPACE = struct (* Names *) val distinct_compsN = "distinct_names" val namespaceN = "_namespace" val valuetypesN = "_valuetypes" val projectN = "project" val injectN = "inject" val getN = "get" val putN = "put" val project_injectL = "StateSpaceLocale.project_inject"; (* Library *) fun fold1 f xs = fold f (tl xs) (hd xs) fun fold1' f [] x = x | fold1' f xs _ = fold1 f xs fun sorted_subset eq [] ys = true | sorted_subset eq (x::xs) [] = false | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys else sorted_subset eq (x::xs) ys; type namespace_info = {declinfo: (typ*string) Termtab.table, (* type, name of statespace *) distinctthm: thm Symtab.table, silent: bool }; structure NameSpaceData = Generic_Data ( type T = namespace_info; val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false}; val extend = I; fun merge ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1}, {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T = {declinfo = Termtab.merge (K true) (declinfo1, declinfo2), distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2), silent = silent1 andalso silent2 (* FIXME odd merge *)} ); fun make_namespace_data declinfo distinctthm silent = {declinfo=declinfo,distinctthm=distinctthm,silent=silent}; fun update_declinfo (n,v) ctxt = let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt; in NameSpaceData.put (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt end; fun set_silent silent ctxt = let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt; in NameSpaceData.put (make_namespace_data declinfo distinctthm silent) ctxt end; val get_silent = #silent o NameSpaceData.get; fun expression_no_pos (expr, fixes) : Expression.expression = (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes); fun prove_interpretation_in ctxt_tac (name, expr) thy = thy |> Interpretation.global_sublocale_cmd (name, Position.none) (expression_no_pos expr) [] |> Proof.global_terminal_proof ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE) |> Proof_Context.theory_of fun add_locale name expr elems thy = thy - |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems + |> Expression.add_locale (Binding.name name) (Binding.name name) [] expr elems |> snd |> Local_Theory.exit; fun add_locale_cmd name expr elems thy = thy - |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems + |> Expression.add_locale_cmd (Binding.name name) Binding.empty [] (expression_no_pos expr) elems |> snd |> Local_Theory.exit; type statespace_info = {args: (string * sort) list, (* type arguments *) parents: (typ list * string * string option list) list, (* type instantiation, state-space name, component renamings *) components: (string * typ) list, types: typ list (* range types of state space *) }; structure StateSpaceData = Generic_Data ( type T = statespace_info Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (K true) data; ); fun add_statespace name args parents components types ctxt = StateSpaceData.put (Symtab.update_new (name, {args=args,parents=parents, components=components,types=types}) (StateSpaceData.get ctxt)) ctxt; fun get_statespace ctxt name = Symtab.lookup (StateSpaceData.get ctxt) name; fun mk_free ctxt name = if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name then let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden; in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end else NONE fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name; fun get_comp ctxt name = Option.mapPartial (Termtab.lookup (#declinfo (NameSpaceData.get ctxt))) (mk_free (Context.proof_of ctxt) name); (*** Tactics ***) fun neq_x_y ctxt x y = (let val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x))); val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val tree = Thm.term_of ctree; val x_path = the (DistinctTreeProver.find_tree x tree); val y_path = the (DistinctTreeProver.find_tree y tree); val thm = DistinctTreeProver.distinctTreeProver ctxt dist_thm x_path y_path; in SOME thm end handle Option.Option => NONE) fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) => (case goal of Const (\<^const_name>\Trueprop\, _) $ (Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\HOL.eq\, _) $ (x as Free _) $ (y as Free _))) => (case neq_x_y ctxt x y of SOME neq => resolve_tac ctxt [neq] i | NONE => no_tac) | _ => no_tac)); val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac; val distinct_simproc = Simplifier.make_simproc \<^context> "StateSpace.distinct_simproc" {lhss = [\<^term>\x = y\], proc = fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\HOL.eq\,_) $ (x as Free _) $ (y as Free _) => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) (neq_x_y ctxt x y) | _ => NONE)}; fun interprete_parent name dist_thm_name parent_expr thy = let fun solve_tac ctxt = CSUBGOAL (fn (goal, i) => let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal; in resolve_tac ctxt [rule] i end); fun tac ctxt = Locale.intro_locales_tac {strict = true, eager = true} ctxt [] THEN ALLGOALS (solve_tac ctxt); in thy |> prove_interpretation_in tac (name, parent_expr) end; fun namespace_definition name nameT parent_expr parent_comps new_comps thy = let val all_comps = parent_comps @ new_comps; val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps); val dist_thm_name = distinct_compsN; val dist_thm_full_name = dist_thm_name; fun comps_of_thm thm = Thm.prop_of thm |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free); fun type_attr phi = Thm.declaration_attribute (fn thm => fn context => (case context of Context.Theory _ => context | Context.Proof ctxt => let val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context; val all_names = comps_of_thm thm; fun upd name tt = (case Symtab.lookup tt name of SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names then Symtab.update (name,thm) tt else tt | NONE => Symtab.update (name,thm) tt) val tt' = tt |> fold upd all_names; val context' = Context_Position.set_visible false ctxt addsimprocs [distinct_simproc] |> Context_Position.restore_visible ctxt |> Context.Proof |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}; in context' end)); val attr = Attrib.internal type_attr; val assume = ((Binding.name dist_thm_name, [attr]), [(HOLogic.Trueprop $ (Const (\<^const_name>\all_distinct\, Type (\<^type_name>\tree\, [nameT]) --> HOLogic.boolT) $ DistinctTreeProver.mk_tree (fn n => Free (n, nameT)) nameT (sort fast_string_ord all_comps)), [])]); in thy |> add_locale name ([], vars) [Element.Assumes [assume]] |> Proof_Context.theory_of |> interprete_parent name dist_thm_full_name parent_expr end; fun encode_dot x = if x = #"." then #"_" else x; fun encode_type (TFree (s, _)) = s | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i | encode_type (Type (n,Ts)) = let val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) ""; val n' = String.map encode_dot n; in if Ts'="" then n' else Ts' ^ "_" ^ n' end; fun project_name T = projectN ^"_"^encode_type T; fun inject_name T = injectN ^"_"^encode_type T; fun add_declaration name decl thy = thy - |> Named_Target.init name + |> Named_Target.init [] name |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy) |> Local_Theory.exit_global; fun parent_components thy (Ts, pname, renaming) = let val ctxt = Context.Theory thy; fun rename [] xs = xs | rename (NONE::rs) (x::xs) = x::rename rs xs | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs; val {args, parents, components, ...} = the (Symtab.lookup (StateSpaceData.get ctxt) pname); val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val parent_comps = maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents; val all_comps = rename renaming (parent_comps @ map (apsnd subst) components); in all_comps end; fun statespace_definition state_type args name parents parent_comps components thy = let val full_name = Sign.full_bname thy name; val all_comps = parent_comps @ components; val components' = map (fn (n,T) => (n,(T,full_name))) components; fun parent_expr (prefix, (_, n, rs)) = (suffix namespaceN n, (prefix, (Expression.Positional rs,[]))); val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; in map fst (Typtab.dest tab) end; val Ts = distinct_types (map snd all_comps); val arg_names = map fst args; val valueN = singleton (Name.variant_list arg_names) "'value"; val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name"; val valueT = TFree (valueN, Sign.defaultS thy); val nameT = TFree (nameN, Sign.defaultS thy); val stateT = nameT --> valueT; fun projectT T = valueT --> T; fun injectT T = T --> valueT; val locinsts = map (fn T => (project_injectL, ((encode_type T,false),(Expression.Positional [SOME (Free (project_name T,projectT T)), SOME (Free ((inject_name T,injectT T)))],[])))) Ts; val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn), (Binding.name (inject_name T),NONE,NoSyn)]) Ts; val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts; fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy = let val {args,types,...} = the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types; val expr = ([(suffix valuetypesN name, (prefix, (Expression.Positional (map SOME pars),[])))],[]); in prove_interpretation_in (fn ctxt => ALLGOALS (solve_tac ctxt (Assumption.all_prems_of ctxt))) (suffix valuetypesN name, expr) thy end; fun interprete_parent (prefix, (_, pname, rs)) = let val expr = ([(pname, (prefix, (Expression.Positional rs,[])))],[]) in prove_interpretation_in (fn ctxt => Locale.intro_locales_tac {strict = true, eager = false} ctxt []) (full_name, expr) end; fun declare_declinfo updates lthy phi ctxt = let fun upd_prf ctxt = let fun upd (n,v) = let val nT = Proof_Context.infer_type (Local_Theory.target_of lthy) (n, dummyT) in Context.proof_map (update_declinfo (Morphism.term phi (Free (n,nT)),v)) end; in ctxt |> fold upd updates end; in Context.mapping I upd_prf ctxt end; fun string_of_typ T = Print_Mode.setmp [] (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T; val fixestate = (case state_type of NONE => [] | SOME s => let val fx = Element.Fixes [(Binding.name s,SOME (string_of_typ stateT),NoSyn)]; val cs = Element.Constrains (map (fn (n,T) => (n,string_of_typ T)) ((map (fn (n,_) => (n,nameT)) all_comps) @ constrains)) in [fx,cs] end ) in thy |> namespace_definition (suffix namespaceN name) nameT (parents_expr,[]) (map fst parent_comps) (map fst components) |> Context.theory_map (add_statespace full_name args (map snd parents) components []) |> add_locale (suffix valuetypesN name) (locinsts,locs) [] |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents |> add_locale_cmd name ([(suffix namespaceN full_name ,(("",false),(Expression.Named [],[]))), (suffix valuetypesN full_name,(("",false),(Expression.Named [],[])))],[]) fixestate |> Proof_Context.theory_of |> fold interprete_parent parents |> add_declaration full_name (declare_declinfo components') end; (* prepare arguments *) fun read_typ ctxt raw_T env = let val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; val T = Syntax.read_typ ctxt' raw_T; val env' = Term.add_tfreesT T env; in (T, env') end; fun cert_typ ctxt raw_T env = let val thy = Proof_Context.theory_of ctxt; val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg; val env' = Term.add_tfreesT T env; in (T, env') end; fun gen_define_statespace prep_typ state_space args name parents comps thy = let (* - args distinct - only args may occur in comps and parent-instantiations - number of insts must match parent args - no duplicate renamings - renaming should occur in namespace *) val _ = writeln ("Defining statespace " ^ quote name ^ " ..."); val ctxt = Proof_Context.init_global thy; fun add_parent (prefix, (Ts, pname, rs)) env = let val prefix' = (case prefix of ("", mandatory) => (pname, mandatory) | _ => prefix); val full_pname = Sign.full_bname thy pname; val {args,components,...} = (case get_statespace (Context.Theory thy) full_pname of SOME r => r | NONE => error ("Undefined statespace " ^ quote pname)); val (Ts',env') = fold_map (prep_typ ctxt) Ts env handle ERROR msg => cat_error msg ("The error(s) above occurred in parent statespace specification " ^ quote pname); val err_insts = if length args <> length Ts' then ["number of type instantiation(s) does not match arguments of parent statespace " ^ quote pname] else []; val rnames = map fst rs val err_dup_renamings = (case duplicates (op =) rnames of [] => [] | dups => ["Duplicate renaming(s) for " ^ commas dups]) val cnames = map fst components; val err_rename_unknowns = (case subtract (op =) cnames rnames of [] => [] | rs => ["Unknown components " ^ commas rs]); val rs' = map (AList.lookup (op =) rs o fst) components; val errs =err_insts @ err_dup_renamings @ err_rename_unknowns in if null errs then ((prefix', (Ts', full_pname, rs')), env') else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) end; val (parents',env) = fold_map add_parent parents []; val err_dup_args = (case duplicates (op =) args of [] => [] | dups => ["Duplicate type argument(s) " ^ commas dups]); val err_dup_components = (case duplicates (op =) (map fst comps) of [] => [] | dups => ["Duplicate state-space components " ^ commas dups]); fun prep_comp (n,T) env = let val (T', env') = prep_typ ctxt T env handle ERROR msg => cat_error msg ("The error(s) above occurred in component " ^ quote n) in ((n,T'), env') end; val (comps',env') = fold_map prep_comp comps env; val err_extra_frees = (case subtract (op =) args (map fst env') of [] => [] | extras => ["Extra free type variable(s) " ^ commas extras]); val defaultS = Sign.defaultS thy; val args' = map (fn x => (x, AList.lookup (op =) env x |> the_default defaultS)) args; fun fst_eq ((x:string,_),(y,_)) = x = y; fun snd_eq ((_,t:typ),(_,u)) = t = u; val raw_parent_comps = maps (parent_components thy o snd) parents'; fun check_type (n,T) = (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of [] => [] | [_] => [] | rs => ["Different types for component " ^ quote n ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o snd) rs)]) val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps) val parent_comps = distinct (fst_eq) raw_parent_comps; val all_comps = parent_comps @ comps'; val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of [] => [] | xs => ["Components already defined in parents: " ^ commas_quote xs]); val errs = err_dup_args @ err_dup_components @ err_extra_frees @ err_dup_types @ err_comp_in_parent; in if null errs then thy |> statespace_definition state_space args' name parents' parent_comps comps' else error (cat_lines errs) end handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name); val define_statespace = gen_define_statespace read_typ NONE; val define_statespace_i = gen_define_statespace cert_typ; (*** parse/print - translations ***) local fun map_get_comp f ctxt (Free (name,_)) = (case (get_comp ctxt name) of SOME (T,_) => f T T dummyT | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*))) | map_get_comp _ _ _ = Syntax.free "arbitrary"; fun name_of (Free (n,_)) = n; in fun gen_lookup_tr ctxt s n = (case get_comp (Context.Proof ctxt) n of SOME (T, _) => Syntax.const \<^const_name>\StateFun.lookup\ $ Syntax.free (project_name T) $ Syntax.free n $ s | NONE => if get_silent (Context.Proof ctxt) then Syntax.const \<^const_name>\StateFun.lookup\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.free n $ s else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", [])); fun lookup_tr ctxt [s, x] = (case Term_Position.strip_positions x of Free (n,_) => gen_lookup_tr ctxt s n | _ => raise Match); fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n; fun lookup_tr' ctxt [_ $ Free (prj, _), n as (_ $ Free (name, _)), s] = (case get_comp (Context.Proof ctxt) name of SOME (T, _) => if prj = project_name T then Syntax.const "_statespace_lookup" $ s $ n else raise Match | NONE => raise Match) | lookup_tr' _ _ = raise Match; fun gen_update_tr id ctxt n v s = let fun pname T = if id then \<^const_name>\Fun.id\ else project_name T; fun iname T = if id then \<^const_name>\Fun.id\ else inject_name T; in (case get_comp (Context.Proof ctxt) n of SOME (T, _) => Syntax.const \<^const_name>\StateFun.update\ $ Syntax.free (pname T) $ Syntax.free (iname T) $ Syntax.free n $ (Syntax.const \<^const_name>\K_statefun\ $ v) $ s | NONE => if get_silent (Context.Proof ctxt) then Syntax.const \<^const_name>\StateFun.update\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.free n $ (Syntax.const \<^const_name>\K_statefun\ $ v) $ s else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined", [])) end; fun update_tr ctxt [s, x, v] = (case Term_Position.strip_positions x of Free (n, _) => gen_update_tr false ctxt n v s | _ => raise Match); fun update_tr' ctxt [_ $ Free (prj, _), _ $ Free (inj, _), n as (_ $ Free (name, _)), (Const (k, _) $ v), s] = if Long_Name.base_name k = Long_Name.base_name \<^const_name>\K_statefun\ then (case get_comp (Context.Proof ctxt) name of SOME (T, _) => if inj = inject_name T andalso prj = project_name T then Syntax.const "_statespace_update" $ s $ n $ v else raise Match | NONE => raise Match) else raise Match | update_tr' _ _ = raise Match; end; (*** outer syntax *) local val type_insts = Parse.typ >> single || \<^keyword>\(\ |-- Parse.!!! (Parse.list1 Parse.typ --| \<^keyword>\)\) val comp = Parse.name -- (\<^keyword>\::\ |-- Parse.!!! Parse.typ); fun plus1_unless test scan = scan ::: Scan.repeat (\<^keyword>\+\ |-- Scan.unless test (Parse.!!! scan)); val mapsto = \<^keyword>\=\; val rename = Parse.name -- (mapsto |-- Parse.name); val renames = Scan.optional (\<^keyword>\[\ |-- Parse.!!! (Parse.list1 rename --| \<^keyword>\]\)) []; val parent = Parse_Spec.locale_prefix -- ((type_insts -- Parse.name) || (Parse.name >> pair [])) -- renames >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames))); in val statespace_decl = Parse.type_args -- Parse.name -- (\<^keyword>\=\ |-- ((Scan.repeat1 comp >> pair []) || (plus1_unless comp parent -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 comp)) []))); val _ = Outer_Syntax.command \<^command_keyword>\statespace\ "define state-space as locale context" (statespace_decl >> (fn ((args, name), (parents, comps)) => Toplevel.theory (define_statespace args name parents comps))); end; end; diff --git a/src/HOL/ex/Perm_Fragments.thy b/src/HOL/ex/Perm_Fragments.thy --- a/src/HOL/ex/Perm_Fragments.thy +++ b/src/HOL/ex/Perm_Fragments.thy @@ -1,293 +1,296 @@ (* Author: Florian Haftmann, TU Muenchen *) section \Fragments on permuations\ theory Perm_Fragments imports "HOL-Library.Perm" "HOL-Library.Dlist" begin -unbundle permutation_syntax - - text \On cycles\ +context + includes permutation_syntax +begin + lemma cycle_prod_list: - "\a # as\ = prod_list (map (\b. \a\b\) (rev as))" + "\a # as\ = prod_list (map (\b. \a \ b\) (rev as))" by (induct as) simp_all lemma cycle_append [simp]: "\a # as @ bs\ = \a # bs\ * \a # as\" proof (induct as rule: cycle.induct) case (3 b c as) then have "\a # (b # as) @ bs\ = \a # bs\ * \a # b # as\" by simp - then have "\a # as @ bs\ * \a\b\ = - \a # bs\ * \a # as\ * \a\b\" + then have "\a # as @ bs\ * \a \ b\ = + \a # bs\ * \a # as\ * \a \ b\" by (simp add: ac_simps) - then have "\a # as @ bs\ * \a\b\ * \a\b\ = - \a # bs\ * \a # as\ * \a\b\ * \a\b\" + then have "\a # as @ bs\ * \a \ b\ * \a \ b\ = + \a # bs\ * \a # as\ * \a \ b\ * \a \ b\" by simp then have "\a # as @ bs\ = \a # bs\ * \a # as\" by (simp add: ac_simps) then show "\a # (b # c # as) @ bs\ = \a # bs\ * \a # b # c # as\" by (simp add: ac_simps) qed simp_all lemma affected_cycle: "affected \as\ \ set as" proof (induct as rule: cycle.induct) case (3 a b as) from affected_times - have "affected (\a # as\ * \a\b\) - \ affected \a # as\ \ affected \a\b\" . + have "affected (\a # as\ * \a \ b\) + \ affected \a # as\ \ affected \a \ b\" . moreover from 3 have "affected (\a # as\) \ insert a (set as)" by simp moreover - have "affected \a\b\ \ {a, b}" + have "affected \a \ b\ \ {a, b}" by (cases "a = b") (simp_all add: affected_swap) - ultimately have "affected (\a # as\ * \a\b\) + ultimately have "affected (\a # as\ * \a \ b\) \ insert a (insert b (set as))" by blast then show ?case by auto qed simp_all lemma orbit_cycle_non_elem: assumes "a \ set as" shows "orbit \as\ a = {a}" unfolding not_in_affected_iff_orbit_eq_singleton [symmetric] using assms affected_cycle [of as] by blast lemma inverse_cycle: assumes "distinct as" shows "inverse \as\ = \rev as\" using assms proof (induct as rule: cycle.induct) case (3 a b as) then have *: "inverse \a # as\ = \rev (a # as)\" and distinct: "distinct (a # b # as)" by simp_all show " inverse \a # b # as\ = \rev (a # b # as)\" proof (cases as rule: rev_cases) case Nil with * show ?thesis by (simp add: swap_sym) next case (snoc cs c) with distinct have "distinct (a # b # cs @ [c])" by simp - then have **: "\a\b\ * \c\a\ = \c\a\ * \c\b\" + then have **: "\a \ b\ * \c \ a\ = \c \ a\ * \c \ b\" by transfer (auto simp add: comp_def Fun.swap_def) with snoc * show ?thesis by (simp add: mult.assoc [symmetric]) qed qed simp_all lemma order_cycle_non_elem: assumes "a \ set as" shows "order \as\ a = 1" proof - from assms have "orbit \as\ a = {a}" by (rule orbit_cycle_non_elem) then have "card (orbit \as\ a) = card {a}" by simp then show ?thesis by simp qed lemma orbit_cycle_elem: assumes "distinct as" and "a \ set as" shows "orbit \as\ a = set as" oops \ \(we need rotation here\ lemma order_cycle_elem: assumes "distinct as" and "a \ set as" shows "order \as\ a = length as" oops text \Adding fixpoints\ definition fixate :: "'a \ 'a perm \ 'a perm" where - "fixate a f = (if a \ affected f then f * \apply (inverse f) a\a\ else f)" + "fixate a f = (if a \ affected f then f * \inverse f \$\ a \ a\ else f)" lemma affected_fixate_trivial: assumes "a \ affected f" shows "affected (fixate a f) = affected f" using assms by (simp add: fixate_def) lemma affected_fixate_binary_circle: assumes "order f a = 2" shows "affected (fixate a f) = affected f - {a, apply f a}" (is "?A = ?B") proof (rule set_eqI) interpret bijection "apply f" by standard simp fix b from assms order_greater_eq_two_iff [of f a] have "a \ affected f" by simp moreover have "apply (f ^ 2) a = a" by (simp add: assms [symmetric]) ultimately show "b \ ?A \ b \ ?B" by (cases "b \ {a, apply (inverse f) a}") (auto simp add: in_affected power2_eq_square apply_inverse apply_times fixate_def) qed lemma affected_fixate_no_binary_circle: assumes "order f a > 2" shows "affected (fixate a f) = affected f - {a}" (is "?A = ?B") proof (rule set_eqI) interpret bijection "apply f" by standard simp fix b from assms order_greater_eq_two_iff [of f a] have "a \ affected f" by simp moreover from assms have "apply f (apply f a) \ a" using apply_power_eq_iff [of f 2 a 0] by (simp add: power2_eq_square apply_times) ultimately show "b \ ?A \ b \ ?B" by (cases "b \ {a, apply (inverse f) a}") (auto simp add: in_affected apply_inverse apply_times fixate_def) qed lemma affected_fixate: "affected (fixate a f) \ affected f - {a}" proof - have "a \ affected f \ order f a = 2 \ order f a > 2" by (auto simp add: not_less dest: affected_order_greater_eq_two) then consider "a \ affected f" | "order f a = 2" | "order f a > 2" by blast then show ?thesis apply cases using affected_fixate_trivial [of a f] affected_fixate_binary_circle [of f a] affected_fixate_no_binary_circle [of f a] by auto qed lemma orbit_fixate_self [simp]: "orbit (fixate a f) a = {a}" proof - have "apply (f * inverse f) a = a" by simp then have "apply f (apply (inverse f) a) = a" by (simp only: apply_times comp_apply) then show ?thesis by (simp add: fixate_def not_in_affected_iff_orbit_eq_singleton [symmetric] in_affected apply_times) qed lemma order_fixate_self [simp]: "order (fixate a f) a = 1" proof - have "card (orbit (fixate a f) a) = card {a}" by simp then show ?thesis by (simp only: card_orbit_eq) simp qed lemma assumes "b \ orbit f a" shows "orbit (fixate b f) a = orbit f a" oops lemma assumes "b \ orbit f a" and "b \ a" shows "orbit (fixate b f) a = orbit f a - {b}" oops text \Distilling cycles from permutations\ inductive_set orbits :: "'a perm \ 'a set set" for f where in_orbitsI: "a \ affected f \ orbit f a \ orbits f" lemma orbits_unfold: "orbits f = orbit f ` affected f" by (auto intro: in_orbitsI elim: orbits.cases) lemma in_orbit_affected: assumes "b \ orbit f a" assumes "a \ affected f" shows "b \ affected f" proof (cases "a = b") case True with assms show ?thesis by simp next case False with assms have "{a, b} \ orbit f a" by auto also from assms have "orbit f a \ affected f" by (blast intro!: orbit_subset_eq_affected) finally show ?thesis by simp qed lemma Union_orbits [simp]: "\(orbits f) = affected f" by (auto simp add: orbits.simps intro: in_orbitsI in_orbit_affected) lemma finite_orbits [simp]: "finite (orbits f)" by (simp add: orbits_unfold) lemma card_in_orbits: assumes "A \ orbits f" shows "card A \ 2" using assms by cases (auto dest: affected_order_greater_eq_two) lemma disjoint_orbits: assumes "A \ orbits f" and "B \ orbits f" and "A \ B" shows "A \ B = {}" using \A \ orbits f\ apply cases using \B \ orbits f\ apply cases using \A \ B\ apply (simp_all add: orbit_disjoint) done definition trace :: "'a \ 'a perm \ 'a list" where "trace a f = map (\n. apply (f ^ n) a) [0.. 'a::linorder list" where "seeds f = sorted_list_of_set (Min ` orbits f)" definition cycles :: "'a perm \ 'a::linorder list list" where "cycles f = map (\a. trace a f) (seeds f)" +end + + +text \Misc\ + lemma (in comm_monoid_list_set) sorted_list_of_set: assumes "finite A" shows "list.F (map h (sorted_list_of_set A)) = set.F h A" proof - from distinct_sorted_list_of_set have "set.F h (set (sorted_list_of_set A)) = list.F (map h (sorted_list_of_set A))" by (rule distinct_set_conv_list) with \finite A\ show ?thesis by (simp) qed - -text \Misc\ - primrec subtract :: "'a list \ 'a list \ 'a list" where "subtract [] ys = ys" | "subtract (x # xs) ys = subtract xs (removeAll x ys)" lemma length_subtract_less_eq [simp]: "length (subtract xs ys) \ length ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) then have "length (subtract xs (removeAll x ys)) \ length (removeAll x ys)" . also have "length (removeAll x ys) \ length ys" by simp finally show ?case by simp qed end diff --git a/src/HOL/ex/Specifications_with_bundle_mixins.thy b/src/HOL/ex/Specifications_with_bundle_mixins.thy new file mode 100644 --- /dev/null +++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy @@ -0,0 +1,60 @@ +theory Specifications_with_bundle_mixins + imports "HOL-Library.Perm" +begin + +locale involutory = + includes permutation_syntax + fixes f :: \'a perm\ + assumes involutory: \\x. f \$\ (f \$\ x) = x\ +begin + +lemma + \f * f = 1\ + using involutory + by (simp add: perm_eq_iff apply_sequence) + +end + +context involutory +begin + +thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*) + +end + + +class at_most_two_elems = + includes permutation_syntax + assumes swap_distinct: \a \ b \ \a \ b\ \$\ c \ c\ +begin + +lemma + \card (UNIV :: 'a set) \ 2\ +proof (rule ccontr) + fix a :: 'a + assume \\ card (UNIV :: 'a set) \ 2\ + then have c0: \card (UNIV :: 'a set) \ 3\ + by simp + then have [simp]: \finite (UNIV :: 'a set)\ + using card.infinite by fastforce + from c0 card_Diff1_le [of UNIV a] + have ca: \card (UNIV - {a}) \ 2\ + by simp + then obtain b where \b \ (UNIV - {a})\ + by (metis all_not_in_conv card.empty card_2_iff' le_zero_eq) + with ca card_Diff1_le [of \UNIV - {a}\ b] + have cb: \card (UNIV - {a, b}) \ 1\ and \a \ b\ + by simp_all + then obtain c where \c \ (UNIV - {a, b})\ + by (metis One_nat_def all_not_in_conv card.empty le_zero_eq nat.simps(3)) + then have \a \ c\ \b \ c\ + by auto + with swap_distinct [of a b c] show False + by (simp add: \a \ b\) +qed + +end + +thm swap_distinct (*syntax from permutation_syntax only present in class specification and initial block*) + +end \ No newline at end of file diff --git a/src/Pure/Isar/class_declaration.ML b/src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML +++ b/src/Pure/Isar/class_declaration.ML @@ -1,391 +1,395 @@ (* Title: Pure/Isar/class_declaration.ML Author: Florian Haftmann, TU Muenchen Declaring classes and subclass relations. *) signature CLASS_DECLARATION = sig - val class: binding -> class list -> + val class: binding -> string list -> class list -> Element.context_i list -> theory -> string * local_theory - val class_cmd: binding -> xstring list -> + val class_cmd: binding -> (xstring * Position.T) list -> xstring list -> Element.context list -> theory -> string * local_theory val prove_subclass: tactic -> class -> local_theory -> local_theory val subclass: class -> local_theory -> Proof.state val subclass_cmd: xstring -> local_theory -> Proof.state end; structure Class_Declaration: CLASS_DECLARATION = struct (** class definitions **) local (* calculating class-related rules including canonical interpretation *) fun calculate thy class sups base_sort param_map assm_axiom = let val thy_ctxt = Proof_Context.init_global thy; val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy; val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy; (* instantiation of canonical interpretation *) val a_tfree = (Name.aT, base_sort); val a_type = TFree a_tfree; val param_map_const = (map o apsnd) Const param_map; val param_map_inst = param_map |> map (fn (x, (c, T)) => let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end); val const_morph = Element.instantiate_normalize_morphism ([], param_map_inst); val typ_morph = Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], []) val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt |> Expression.cert_goal_expression ([(class, (("", false), (Expression.Named param_map_const, [])))], []); val (props, inst_morph) = if null param_map then (raw_props |> map (Morphism.term typ_morph), raw_inst_morph $> typ_morph) else (raw_props, raw_inst_morph); (*FIXME proper handling in locale.ML / expression.ML would be desirable*) (* witness for canonical interpretation *) val some_prop = try the_single props; val some_witn = Option.map (fn prop => let val sup_axioms = map_filter (fst o Class.rules thy) sups; val loc_intro_tac = (case Locale.intros_of thy class of (_, NONE) => all_tac | (_, SOME intro) => ALLGOALS (resolve_tac thy_ctxt [intro])); val tac = loc_intro_tac THEN ALLGOALS (Proof_Context.fact_tac thy_ctxt (sup_axioms @ the_list assm_axiom)); in Element.prove_witness thy_ctxt prop tac end) some_prop; val some_axiom = Option.map (Element.conclude_witness thy_ctxt) some_witn; (* canonical interpretation *) val base_morph = inst_morph $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class)) $> Element.satisfy_morphism (the_list some_witn); val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups); (* assm_intro *) fun prove_assm_intro thm = let val ((_, [thm']), _) = Variable.import true [thm] thy_ctxt; val const_eq_morph = (case eq_morph of SOME eq_morph => const_morph $> eq_morph | NONE => const_morph); val thm'' = Morphism.thm const_eq_morph thm'; in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm''])) end; val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class)); (* of_class *) val of_class_prop_concl = Logic.mk_of_class (a_type, class); val of_class_prop = (case some_prop of NONE => of_class_prop_concl | SOME prop => Logic.mk_implies (Morphism.term const_morph ((map_types o map_atyps) (K a_type) prop), of_class_prop_concl)); val sup_of_classes = map (snd o Class.rules thy) sups; val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); val axclass_intro = #intro (Axclass.get_info thy class); val base_sort_trivs = Thm.of_sort (Thm.global_ctyp_of thy a_type, base_sort); fun tac ctxt = REPEAT (SOMEGOAL (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) ORELSE' assume_tac ctxt)); val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context); in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end; (* reading and processing class specifications *) -fun prep_class_elems prep_decl thy sups raw_elems = +fun prep_class_elems prep_decl ctxt sups raw_elems = let (* user space type system: only permits 'a type variable, improves towards 'a *) + val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val inter_sort = curry (Sorts.inter_sort algebra); val proto_base_sort = if null sups then Sign.defaultS thy else fold inter_sort (map (Class.base_sort thy) sups) []; val is_param = member (op =) (map fst (Class.these_params thy sups)); val base_constraints = (map o apsnd) (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd) (Class.these_operations thy sups); val singleton_fixate = burrow_types (fn Ts => let val tfrees = fold Term.add_tfreesT Ts []; val inferred_sort = (fold o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts []; val fixate_sort = (case tfrees of [] => inferred_sort | [(a, S)] => if a <> Name.aT then error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") else if Sorts.sort_le algebra (S, inferred_sort) then S else error ("Type inference imposes additional sort constraint " ^ Syntax.string_of_sort_global thy inferred_sort ^ " of type parameter " ^ Name.aT ^ " of sort " ^ Syntax.string_of_sort_global thy S) | _ => error "Multiple type variables in class specification"); val fixateT = Term.aT fixate_sort; in (map o map_atyps) (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts end); fun unify_params ts = let val param_Ts = (fold o fold_aterms) (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts []; val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts; val param_T = if null param_namesT then NONE else SOME (case get_first (try dest_TFree) param_Ts of SOME v_sort => TFree v_sort | NONE => TVar (hd param_namesT, proto_base_sort)); in case param_T of NONE => ts | SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts end; (* preprocessing elements, retrieving base sort from type-checked elements *) val raw_supexpr = (map (fn sup => (sup, (("", false), (Expression.Positional [], [])))) sups, []); val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate)); val ((raw_supparams, _, raw_inferred_elems, _), _) = - Proof_Context.init_global thy + ctxt |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params)) |> prep_decl raw_supexpr init_class_body raw_elems; fun filter_element (Element.Fixes []) = NONE | filter_element (e as Element.Fixes _) = SOME e | filter_element (Element.Constrains []) = NONE | filter_element (e as Element.Constrains _) = SOME e | filter_element (Element.Assumes []) = NONE | filter_element (e as Element.Assumes _) = SOME e | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.") | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.") | filter_element (Element.Lazy_Notes _) = error ("\"notes\" element not allowed in class specification."); val inferred_elems = map_filter filter_element raw_inferred_elems; fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => fold_types f t #> (fold o fold_types) f ts) o snd) assms; val base_sort = if null inferred_elems then proto_base_sort else (case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of [] => error "No type variable in class specification" | [(_, sort)] => sort | _ => error "Multiple type variables in class specification"); val supparams = map (fn ((c, T), _) => (c, map_atyps (K (Term.aT base_sort)) T)) raw_supparams; val supparam_names = map fst supparams; fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); val supexpr = (map (fn sup => (sup, (("", false), (Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup)), [])))) sups, map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); in (base_sort, supparam_names, supexpr, inferred_elems) end; val cert_class_elems = prep_class_elems Expression.cert_declaration; val read_class_elems = prep_class_elems Expression.cert_read_declaration; -fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems = +fun prep_class_spec prep_class prep_include prep_class_elems ctxt raw_supclasses raw_includes raw_elems = let - val thy_ctxt = Proof_Context.init_global thy; + val thy = Proof_Context.theory_of ctxt; (* prepare import *) val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses); + val sups = Sign.minimize_sort thy (map (prep_class ctxt) raw_supclasses); val _ = (case filter_out (Class.is_class thy) sups of [] => () | no_classes => error ("No (proper) classes: " ^ commas_quote no_classes)); val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups); val raw_supparam_names = map fst raw_supparams; val _ = if has_duplicates (op =) raw_supparam_names then error ("Duplicate parameter(s) in superclasses: " ^ (commas_quote (duplicates (op =) raw_supparam_names))) else (); (* infer types and base sort *) - val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems; + val includes = map (prep_include ctxt) raw_includes; + val includes_ctxt = Bundle.includes includes ctxt; + val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems includes_ctxt sups raw_elems; val sup_sort = inter_sort base_sort sups; (* process elements as class specification *) - val class_ctxt = Class.begin sups base_sort thy_ctxt; + val class_ctxt = Class.begin sups base_sort includes_ctxt; val ((_, _, syntax_elems, _), _) = class_ctxt |> Expression.cert_declaration supexpr I inferred_elems; fun check_vars e vs = if null vs then error ("No type variable in part of specification element " ^ Pretty.string_of (Pretty.chunks (Element.pretty_ctxt class_ctxt e))) else (); fun check_element (e as Element.Fixes fxs) = List.app (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs | check_element (e as Element.Assumes assms) = List.app (fn (_, ts_pss) => List.app (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms | check_element _ = (); val _ = List.app check_element syntax_elems; fun fork_syn (Element.Fixes xs) = fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs #>> Element.Fixes | fork_syn x = pair x; val (elems, global_syntax) = fold_map fork_syn syntax_elems []; - in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end; + in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end; -val cert_class_spec = prep_class_spec (K I) cert_class_elems; -val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems; +val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems; +val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check read_class_elems; (* class establishment *) fun add_consts class base_sort sups supparam_names global_syntax thy = let (*FIXME simplify*) val supconsts = supparam_names |> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups)) |> (map o apsnd o apsnd o map_atyps) (K (Term.aT [class])); val all_params = Locale.params_of thy class; val raw_params = (snd o chop (length supparam_names)) all_params; fun add_const ((raw_c, raw_ty), _) thy = let val b = Binding.name raw_c; val c = Sign.full_name thy b; val ty = map_atyps (K (Term.aT base_sort)) raw_ty; val ty0 = Type.strip_sorts ty; val ty' = map_atyps (K (Term.aT [class])) ty0; val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; in thy |> Sign.declare_const_global ((b, ty0), syn) |> snd |> pair ((Variable.check_name b, ty), (c, ty')) end; in thy |> Sign.add_path (Class.class_prefix class) |> fold_map add_const raw_params ||> Sign.restore_naming thy |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) end; fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy = let (*FIXME simplify*) fun globalize param_map = map_aterms (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) | t => t); val raw_pred = Locale.intros_of thy class |> fst |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); fun get_axiom thy = (case #axioms (Axclass.get_info thy class) of [] => NONE | [thm] => SOME thm); in thy |> add_consts class base_sort sups supparam_names global_syntax |-> (fn (param_map, params) => Axclass.define_class (bname, supsort) (map (fst o snd) params) [(Binding.empty_atts, Option.map (globalize param_map) raw_pred |> the_list)] #> snd #> `get_axiom #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params #> pair (param_map, params, assm_axiom))) end; -fun gen_class prep_class_spec b raw_supclasses raw_elems thy = +fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy = let val class = Sign.full_name thy b; val prefix = Binding.qualify true "class"; - val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) = - prep_class_spec thy raw_supclasses raw_elems; + val ctxt = Proof_Context.init_global thy; + val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) = + prep_class_spec ctxt raw_supclasses raw_includes raw_elems; in thy - |> Expression.add_locale b (prefix b) supexpr elems + |> Expression.add_locale b (prefix b) includes supexpr elems |> snd |> Local_Theory.exit_global |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate thy class sups base_sort param_map assm_axiom) #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) => Locale.add_registration_theory' {inst = (class, base_morph), mixin = Option.map (rpair true) eq_morph, export = export_morph} #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |> snd - |> Named_Target.init class + |> Named_Target.init includes class |> pair class end; in val class = gen_class cert_class_spec; val class_cmd = gen_class read_class_spec; end; (*local*) (** subclass relations **) local fun gen_subclass prep_class do_proof raw_sup lthy = let val thy = Proof_Context.theory_of lthy; val proto_sup = prep_class thy raw_sup; val proto_sub = (case Named_Target.class_of lthy of SOME class => class | NONE => error "Not in a class target"); val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup); val expr = ([(sup, (("", false), (Expression.Positional [], [])))], []); val (([props], _, deps, _, export), goal_ctxt) = Expression.cert_goal_expression expr lthy; val some_prop = try the_single props; val some_dep_morph = try the_single (map snd deps); fun after_qed some_wit = Class.register_subclass (sub, sup) some_dep_morph some_wit export; in do_proof after_qed some_prop goal_ctxt end; fun user_proof after_qed some_prop = Element.witness_proof (after_qed o try the_single o the_single) [the_list some_prop]; fun tactic_proof tac after_qed some_prop ctxt = after_qed (Option.map (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; in fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); fun subclass x = gen_subclass (K I) user_proof x; fun subclass_cmd x = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof x; end; (*local*) end; diff --git a/src/Pure/Isar/experiment.ML b/src/Pure/Isar/experiment.ML --- a/src/Pure/Isar/experiment.ML +++ b/src/Pure/Isar/experiment.ML @@ -1,45 +1,45 @@ (* Title: Pure/Isar/experiment.ML Author: Makarius Target for specification experiments that are mostly private. *) signature EXPERIMENT = sig val is_experiment: theory -> string -> bool val experiment: Element.context_i list -> theory -> Binding.scope * local_theory val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory end; structure Experiment: EXPERIMENT = struct structure Data = Theory_Data ( type T = Symtab.set; val empty = Symtab.empty; val extend = I; val merge = Symtab.merge (K true); ); fun is_experiment thy name = Symtab.defined (Data.get thy) name; fun gen_experiment add_locale elems thy = let val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; val lthy = thy - |> add_locale experiment_name Binding.empty ([], []) elems + |> add_locale experiment_name Binding.empty [] ([], []) elems |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set); val (scope, naming) = Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); val naming' = naming |> Name_Space.private_scope scope; val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) |> Local_Theory.map_background_naming Name_Space.concealed; in (scope, lthy') end; val experiment = gen_experiment Expression.add_locale; val experiment_cmd = gen_experiment Expression.add_locale_cmd; end; diff --git a/src/Pure/Isar/expression.ML b/src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML +++ b/src/Pure/Isar/expression.ML @@ -1,872 +1,877 @@ (* Title: Pure/Isar/expression.ML Author: Clemens Ballarin, TU Muenchen Locale expressions and user interface layer of locales. *) signature EXPRESSION = sig (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list type 'term rewrites = (Attrib.binding * 'term) list type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list type expression_i = (string, term) expr * (binding * typ option * mixfix) list type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list (* Processing of context statements *) val cert_statement: Element.context_i list -> Element.statement_i -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context val read_statement: Element.context list -> Element.statement -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context (* Declaring locales *) val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) - val add_locale: binding -> binding -> + val add_locale: binding -> binding -> string list -> expression_i -> Element.context_i list -> theory -> string * local_theory - val add_locale_cmd: binding -> binding -> + val add_locale_cmd: binding -> binding -> (xstring * Position.T) list -> expression -> Element.context list -> theory -> string * local_theory (* Processing of locale expressions *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context end; structure Expression : EXPRESSION = struct datatype ctxt = datatype Element.ctxt; (*** Expressions ***) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list; type 'term rewrites = (Attrib.binding * 'term) list; type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list; type expression_i = (string, term) expr * (binding * typ option * mixfix) list; type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list; (** Internalise locale names in expr **) fun check_expr thy instances = map (apfst (Locale.check thy)) instances; (** Parameters of expression **) (*Sanity check of instantiations and extraction of implicit parameters. The latter only occurs iff strict = false. Positional instantiations are extended to match full length of parameter list of instantiated locale.*) fun parameters_of thy strict (expr, fixed) = let val ctxt = Proof_Context.init_global thy; fun reject_dups message xs = (case duplicates (op =) xs of [] => () | dups => error (message ^ commas dups)); fun parm_eq ((p1, mx1), (p2, mx2)) = p1 = p2 andalso (Mixfix.equal (mx1, mx2) orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); fun params_inst (loc, (prfx, (Positional insts, eqns))) = let val ps = params_loc loc; val d = length ps - length insts; val insts' = if d < 0 then error ("More arguments than parameters in instantiation of locale " ^ quote (Locale.markup_name ctxt loc)) else insts @ replicate d NONE; val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); in (ps', (loc, (prfx, (Positional insts', eqns)))) end | params_inst (loc, (prfx, (Named insts, eqns))) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " (map fst insts); val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps else error (quote p ^ " not a parameter of instantiated expression")); in (ps', (loc, (prfx, (Named insts, eqns)))) end; fun params_expr is = let val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; val fixed' = map (Variable.check_name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] else let val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed'); in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; in (expr', implicit'' @ fixed) end; (** Read instantiation **) (* Parse positional or named instantiation *) local fun prep_inst prep_term ctxt parms (Positional insts) = (insts ~~ parms) |> map (fn (NONE, p) => Free (p, dummyT) | (SOME t, _) => prep_term ctxt t) | prep_inst prep_term ctxt parms (Named insts) = parms |> map (fn p => (case AList.lookup (op =) insts p of SOME t => prep_term ctxt t | NONE => Free (p, dummyT))); in fun parse_inst x = prep_inst Syntax.parse_term x; fun make_inst x = prep_inst (K I) x; end; (* Instantiation morphism *) fun inst_morphism params ((prfx, mandatory), insts') ctxt = let (* parameters *) val parm_types = map #2 params; val type_parms = fold Term.add_tfreesT parm_types []; (* type inference *) val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; val type_parms' = fold Term.add_tvarsT parm_types' []; val checked = (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) val (type_parms'', insts'') = chop (length type_parms') checked; (* context *) val ctxt' = fold Proof_Context.augment checked ctxt; val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; (* instantiation *) val instT = (type_parms ~~ map Logic.dest_type type_parms'') |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); val cert_inst = ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); in (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; (*** Locale processing ***) (** Parsing **) fun parse_elem prep_typ prep_term ctxt = Element.map_ctxt {binding = I, typ = prep_typ ctxt, term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), fact = I, attrib = I}; fun prepare_stmt prep_prop prep_obtains ctxt stmt = (case stmt of Element.Shows raw_shows => raw_shows |> (map o apsnd o map) (fn (t, ps) => (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) | Element.Obtains raw_obtains => let val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; val obtains = prep_obtains thesis_ctxt thesis raw_obtains; in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); (** Simultaneous type inference: instantiations + elements + statement **) local fun mk_type T = (Logic.mk_type T, []); fun mk_term t = (t, []); fun mk_propp (p, pats) = (Type.constraint propT p, pats); fun dest_type (T, []) = Logic.dest_type T; fun dest_term (t, []) = t; fun dest_propp (p, pats) = (p, pats); fun extract_inst (_, (_, ts)) = map mk_term ts; fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)); fun extract_eqns es = map (mk_term o snd) es; fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs; fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs | extract_elem (Notes _) = [] | extract_elem (Lazy_Notes _) = []; fun restore_elem (Fixes fixes, css) = (fixes ~~ css) |> map (fn ((x, _, mx), cs) => (x, cs |> map dest_type |> try hd, mx)) |> Fixes | restore_elem (Constrains csts, css) = (csts ~~ css) |> map (fn ((x, _), cs) => (x, cs |> map dest_type |> hd)) |> Constrains | restore_elem (Assumes asms, css) = (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes | restore_elem (Defines defs, css) = (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines | restore_elem (elem as Notes _, _) = elem | restore_elem (elem as Lazy_Notes _, _) = elem; fun prep (_, pats) (ctxt, t :: ts) = let val ctxt' = Proof_Context.augment t ctxt in ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), (ctxt', ts)) end; fun check cs ctxt = let val (cs', (ctxt', _)) = fold_map prep cs (ctxt, Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)); in (cs', ctxt') end; in fun check_autofix insts eqnss elems concl ctxt = let val inst_cs = map extract_inst insts; val eqns_cs = map extract_eqns eqnss; val elem_css = map extract_elem elems; val concl_cs = (map o map) mk_propp (map snd concl); (* Type inference *) val (inst_cs' :: eqns_cs' :: css', ctxt') = (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in ((map restore_inst (insts ~~ inst_cs'), map restore_eqns (eqnss ~~ eqns_cs'), map restore_elem (elems ~~ elem_css'), map fst concl ~~ concl_cs'), ctxt') end; end; (** Prepare locale elements **) fun declare_elem prep_var (Fixes fixes) ctxt = let val (vars, _) = fold_map prep_var fixes ctxt in ctxt |> Proof_Context.add_fixes vars |> snd end | declare_elem prep_var (Constrains csts) ctxt = ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd | declare_elem _ (Assumes _) ctxt = ctxt | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt | declare_elem _ (Lazy_Notes _) ctxt = ctxt; (** Finish locale elements **) fun finish_inst ctxt (loc, (prfx, inst)) = let val thy = Proof_Context.theory_of ctxt; val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; in (loc, morph) end; fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => let val x = Binding.name_of binding in (binding, AList.lookup (op =) parms x, mx) end); local fun closeup _ _ false elem = elem | closeup (outer_ctxt, ctxt) parms true elem = let (* FIXME consider closing in syntactic phase -- before type checking *) fun close_frees t = let val rev_frees = Term.fold_aterms (fn Free (x, T) => if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t []; in fold (Logic.all o Free) rev_frees t end; fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in context element"; in (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) | e => e) end; in fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes) | finish_elem _ _ _ (Constrains _) = Constrains [] | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms) | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs) | finish_elem _ _ _ (elem as Notes _) = elem | finish_elem _ _ _ (elem as Lazy_Notes _) = elem; end; (** Process full context statement: instantiations + elements + statement **) (* Interleave incremental parsing and type inference over entire parsed stretch. *) local fun abs_def ctxt = Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; fun prep_full_context_statement parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 = let val thy = Proof_Context.theory_of ctxt1; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let val params = map #1 (Locale.params_of thy loc); val inst' = prep_inst ctxt (map #1 params) inst; val parm_types' = params |> map (#2 #> Logic.varifyT_global #> Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> Type_Infer.paramify_vars); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt; val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 handle ERROR msg => if null eqns then error msg else (Locale.tracing ctxt1 (msg ^ "\nFalling back to reading rewrites clause before activation."); ctxt2); val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns; val eqns' = (prep_eqns ctxt' o map snd) eqns; val eqnss' = [attrss ~~ eqns']; val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt'; val rewrite_morph = eqns' |> map (abs_def ctxt') |> Variable.export_terms ctxt' ctxt |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity; val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']; in (i + 1, insts', eqnss', ctxt'') end; fun prep_elem raw_elem ctxt = let val ctxt' = ctxt |> Context_Position.set_visible false |> declare_elem prep_var_elem raw_elem |> Context_Position.restore_visible ctxt; val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem; in (elems', ctxt') end; val fors = fold_map prep_var_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd; val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2); fun prep_stmt elems ctxt = check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; val _ = if fixed_frees then () else (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of [] => () | frees => error ("Illegal free variables in expression: " ^ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); val ((insts, _, elems', concl), ctxt4) = ctxt3 |> init_body |> fold_map prep_elem raw_elems |-> prep_stmt; (* parameters from expression and elements *) val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) (Fixes fors :: elems'); val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4; val fors' = finish_fixes parms fors; val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors'; val deps = map (finish_inst ctxt5) insts; val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'; in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end; in fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) Obtain.cert_obtains Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x; end; (* Context statement: elements + statement *) local fun prep_statement prep activate raw_elems raw_stmt ctxt = let val ((_, _, _, elems, concl), _) = prep {strict = true, do_close = false, fixed_frees = true} ([], []) I raw_elems raw_stmt ctxt; val ctxt' = ctxt |> Proof_Context.set_stmt true |> fold_map activate elems |> #2 |> Proof_Context.restore_stmt ctxt; in (concl, ctxt') end; in fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x; fun read_statement x = prep_statement read_full_context_statement Element.activate x; end; (* Locale declaration: import + elements *) fun fix_params params = Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; local fun prep_declaration prep activate raw_import init_body raw_elems ctxt = let val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) = prep {strict = false, do_close = true, fixed_frees = false} raw_import init_body raw_elems (Element.Shows []) ctxt; val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale"; (* Declare parameters and imported facts *) val ctxt' = ctxt |> fix_params fixed |> fold (Context.proof_map o Locale.activate_facts NONE) deps; val (elems', ctxt'') = ctxt' |> Proof_Context.set_stmt true |> fold_map activate elems ||> Proof_Context.restore_stmt ctxt'; in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end; in fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; fun read_declaration x = prep_declaration read_full_context_statement Element.activate x; end; (* Locale expression to set up a goal *) local fun props_of thy (name, morph) = let val (asm, defs) = Locale.specification_of thy name in map (Morphism.term morph) (the_list asm @ defs) end; fun prep_goal_expression prep expression ctxt = let val thy = Proof_Context.theory_of ctxt; val ((fixed, deps, eqnss, _, _), _) = prep {strict = true, do_close = true, fixed_frees = true} expression I [] (Element.Shows []) ctxt; (* proof obligations *) val propss = map (props_of thy) deps; val eq_propss = (map o map) snd eqnss; val goal_ctxt = ctxt |> fix_params fixed |> (fold o fold) Proof_Context.augment (propss @ eq_propss); val export = Proof_Context.export_morphism goal_ctxt ctxt; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism "Expression.prep_goal" {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]}; in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end; in fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; fun read_goal_expression x = prep_goal_expression read_full_context_statement x; end; (*** Locale declarations ***) (* extract specification text *) val norm_term = Envir.beta_norm oo Term.subst_atomic; fun bind_def ctxt eq (xs, env, eqs) = let val _ = Local_Defs.cert_def ctxt (K []) eq; val ((y, T), b) = Local_Defs.abs_def eq; val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) | dups => if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs) else err "Attempt to redefine variable") end; (* text has the following structure: (((exts, exts'), (ints, ints')), (xs, env, defs)) where exts: external assumptions (terms in assumes elements) exts': dito, normalised wrt. env ints: internal assumptions (terms in assumptions from insts) ints': dito, normalised wrt. env xs: the free variables in exts' and ints' and rhss of definitions, this includes parameters except defined parameters env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env defs: the equations from the defines elements *) fun eval_text _ _ (Fixes _) text = text | eval_text _ _ (Constrains _) text = text | eval_text _ is_ext (Assumes asms) (((exts, exts'), (ints, ints')), (xs, env, defs)) = let val ts = maps (map #1 o #2) asms; val ts' = map (norm_term env) ts; val spec' = if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) else ((exts, exts'), (ints @ ts, ints' @ ts')); in (spec', (fold Term.add_frees ts' xs, env, defs)) end | eval_text ctxt _ (Defines defs) (spec, binds) = (spec, fold (bind_def ctxt o #1 o #2) defs binds) | eval_text _ _ (Notes _) text = text | eval_text _ _ (Lazy_Notes _) text = text; fun eval_inst ctxt (loc, morph) text = let val thy = Proof_Context.theory_of ctxt; val (asm, defs) = Locale.specification_of thy loc; val asm' = Option.map (Morphism.term morph) asm; val defs' = map (Morphism.term morph) defs; val text' = text |> (if is_some asm then eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])]) else I) |> (if not (null defs) then eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs')) else I) (* FIXME clone from locale.ML *) in text' end; fun eval_elem ctxt elem text = eval_text ctxt true elem text; fun eval ctxt deps elems = let val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], [])); val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text'; in (spec, defs) end; (* axiomsN: name of theorem set with destruct rules for locale predicates, also name suffix of delta predicates and assumptions. *) val axiomsN = "axioms"; local (* introN: name of theorems for introduction rules of locale and delta predicates *) val introN = "intro"; fun atomize_spec ctxt ts = let val t = Logic.mk_conjunction_balanced ts; val body = Object_Logic.atomize_term ctxt t; val bodyT = Term.fastype_of body; in if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t)) else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t)) end; (* achieve plain syntax for locale predicates (without "PROP") *) fun aprop_tr' n c = let val c' = Lexicon.mark_const c; fun tr' (_: Proof.context) T args = if T <> dummyT andalso length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args) else raise Match; in (c', tr') end; (* define one predicate including its intro rule and axioms - binding: predicate name - parms: locale parameters - defs: thms representing substitutions from defines elements - ts: terms representing locale assumptions (not normalised wrt. defs) - norm_ts: terms representing locale assumptions (normalised wrt. defs) - thy: the theory *) fun def_pred binding parms defs ts norm_ts thy = let val name = Sign.full_name thy binding; val thy_ctxt = Proof_Context.init_global thy; val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts; val env = Term.add_free_names body []; val xs = filter (member (op =) env o #1) parms; val Ts = map #2 xs; val extraTs = (subtract (op =) (fold Term.add_tfreesT Ts []) (Term.add_tfrees body [])) |> sort_by #1 |> map TFree; val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; val args = map Logic.mk_type extraTs @ map Free xs; val head = Term.list_comb (Const (name, predT), args); val statement = Object_Logic.ensure_propT thy_ctxt head; val ([pred_def], defs_thy) = thy |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name] |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])]; val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head; val intro = Goal.prove_global defs_thy [] norm_ts statement (fn {context = ctxt, ...} => rewrite_goals_tac ctxt [pred_def] THEN compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts)); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness axioms_ctxt t (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1)); in ((statement, intro, axioms), defs_thy) end; in (* main predicate definition function *) fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy = let val ctxt = Proof_Context.init_global thy; val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs; val (a_pred, a_intro, a_axioms, thy'') = if null exts then (NONE, NONE, [], thy) else let val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding; val ((statement, intro, axioms), thy') = thy |> def_pred abinding parms defs' exts exts'; val ((_, [intro']), thy'') = thy' |> Sign.qualified_path true abinding |> Global_Theory.note_thms "" ((Binding.name introN, []), [([intro], [Locale.unfold_add])]) ||> Sign.restore_naming thy'; in (SOME statement, SOME intro', axioms, thy'') end; val (b_pred, b_intro, b_axioms, thy'''') = if null ints then (NONE, NONE, [], thy'') else let val ((statement, intro, axioms), thy''') = thy'' |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val ctxt''' = Proof_Context.init_global thy'''; val ([(_, [intro']), _], thy'''') = thy''' |> Sign.qualified_path true binding |> Global_Theory.note_thmss "" [((Binding.name introN, []), [([intro], [Locale.intro_add])]), ((Binding.name axiomsN, []), [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms, [])])] ||> Sign.restore_naming thy'''; in (SOME statement, SOME intro', axioms, thy'''') end; in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end; end; local fun assumes_to_notes (Assumes asms) axms = fold_map (fn (a, spec) => fn axs => let val (ps, qs) = chop (length spec) axs in ((a, [(ps, [])]), qs) end) asms axms |> apfst (curry Notes "") | assumes_to_notes e axms = (e, axms); fun defines_to_notes ctxt (Defines defs) = Notes ("", map (fn (a, (def, _)) => (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)], [(Attrib.internal o K) Locale.witness_add])])) defs) | defines_to_notes _ e = e; val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false; -fun gen_add_locale prep_decl - binding raw_predicate_binding raw_import raw_body thy = +fun gen_add_locale prep_include prep_decl + binding raw_predicate_binding raw_includes raw_import raw_body thy = let val name = Sign.full_name thy binding; val _ = Locale.defined thy name andalso error ("Duplicate definition of locale " ^ quote name); + val ctxt = Proof_Context.init_global thy; + val includes = map (prep_include ctxt) raw_includes; + val ((fixed, deps, body_elems, _), (parms, ctxt')) = - prep_decl raw_import I raw_body (Proof_Context.init_global thy); + ctxt + |> Bundle.includes includes + |> prep_decl raw_import I raw_body; val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []); val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ Binding.print binding ^ ": " ^ commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs))); val predicate_binding = if Binding.is_empty raw_predicate_binding then binding else raw_predicate_binding; val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_binding parms text thy; val pred_ctxt = Proof_Context.init_global thy'; val a_satisfy = Element.satisfy_morphism a_axioms; val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ maps (fn Fixes fixes => map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems; val asm = if is_some b_statement then b_statement else a_statement; val hyp_spec = filter is_hyp body_elems; val notes = if is_some asm then [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []), [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))], [(Attrib.internal o K) Locale.witness_add])])])] else []; val notes' = body_elems |> map (defines_to_notes pred_ctxt) |> map (Element.transform_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |> fst |> map (Element.transform_ctxt b_satisfy) |> map_filter (fn Notes notes => SOME notes | _ => NONE); val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val axioms = map (Element.conclude_witness pred_ctxt) b_axioms; val loc_ctxt = thy' |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps') - |> Named_Target.init name + |> Named_Target.init includes name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; in -val add_locale = gen_add_locale cert_declaration; -val add_locale_cmd = gen_add_locale read_declaration; +val add_locale = gen_add_locale (K I) cert_declaration; +val add_locale_cmd = gen_add_locale Bundle.check read_declaration; end; end; diff --git a/src/Pure/Isar/interpretation.ML b/src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML +++ b/src/Pure/Isar/interpretation.ML @@ -1,237 +1,237 @@ (* Title: Pure/Isar/interpretation.ML Author: Clemens Ballarin, TU Muenchen Author: Florian Haftmann, TU Muenchen Locale interpretation. *) signature INTERPRETATION = sig type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (*interpretation in proofs*) val interpret: Expression.expression_i -> Proof.state -> Proof.state val interpret_cmd: Expression.expression -> Proof.state -> Proof.state (*interpretation in local theories*) val interpretation: Expression.expression_i -> local_theory -> Proof.state val interpretation_cmd: Expression.expression -> local_theory -> Proof.state (*interpretation into global theories*) val global_interpretation: Expression.expression_i -> term defines -> local_theory -> Proof.state val global_interpretation_cmd: Expression.expression -> string defines -> local_theory -> Proof.state (*interpretation between locales*) val sublocale: Expression.expression_i -> term defines -> local_theory -> Proof.state val sublocale_cmd: Expression.expression -> string defines -> local_theory -> Proof.state val global_sublocale: string -> Expression.expression_i -> term defines -> theory -> Proof.state val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> string defines -> theory -> Proof.state (*mixed Isar interface*) val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state end; structure Interpretation : INTERPRETATION = struct (** common interpretation machinery **) type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (* reading of locale expressions with rewrite morphisms *) local fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy = let val rhs = prep_term lthy raw_rhs; val lthy' = Variable.declare_term rhs lthy; val ((_, (_, def)), lthy'') = Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy'; in (Thm.symmetric def, lthy'') end; fun augment_with_defs _ [] _ = pair [] (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) | augment_with_defs prep_term raw_defs deps = Local_Theory.begin_nested #> snd #> fold Locale.activate_declarations deps #> fold_map (augment_with_def prep_term) raw_defs #> Local_Theory.end_nested_result Morphism.fact; fun prep_interpretation prep_expr prep_term expression raw_defs initial_ctxt = let val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; val (def_eqns, def_ctxt) = augment_with_defs prep_term raw_defs deps expr_ctxt; val export' = Proof_Context.export_morphism def_ctxt expr_ctxt; in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; in fun cert_interpretation expression = prep_interpretation Expression.cert_goal_expression Syntax.check_term expression; fun read_interpretation expression = prep_interpretation Expression.read_goal_expression Syntax.read_term expression; end; (* interpretation machinery *) local fun abs_def_rule eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); fun note_eqns_register note add_registration deps eqnss witss def_eqns thms export export' ctxt = let val factss = thms |> unflat ((map o map) #1 eqnss) |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt; val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; val deps' = (deps ~~ witss) |> map (fn ((dep, morph), wits) => (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); fun register (dep, eqns) ctxt = ctxt |> add_registration {inst = dep, mixin = Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), export = export}; in ctxt'' |> fold register (deps' ~~ eqnss') end; in fun generic_interpretation prep_interpretation setup_proof note add_registration expression raw_defs initial_ctxt = let val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = prep_interpretation expression raw_defs initial_ctxt; fun after_qed witss eqns = note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; end; (** interfaces **) (* interpretation in proofs *) local fun setup_proof state after_qed propss eqns goal_ctxt = Element.witness_local_proof_eqs (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) "interpret" propss eqns goal_ctxt state; fun gen_interpret prep_interpretation expression state = Proof.assert_forward_or_chain state |> Proof.context_of |> generic_interpretation prep_interpretation (setup_proof state) Attrib.local_notes Locale.add_registration_proof expression []; in val interpret = gen_interpret cert_interpretation; val interpret_cmd = gen_interpret read_interpretation; end; (* interpretation in local theories *) fun interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Locale.add_registration_local_theory expression []; fun interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Locale.add_registration_local_theory expression []; (* interpretation into global theories *) fun global_interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; fun global_interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; (* interpretation between locales *) fun sublocale expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; fun sublocale_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; local fun gen_global_sublocale prep_loc prep_interpretation raw_locale expression raw_defs thy = let - val lthy = Named_Target.init (prep_loc thy raw_locale) thy; + val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy; fun setup_proof after_qed = Element.witness_proof_eqs (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); in lthy |> generic_interpretation prep_interpretation setup_proof Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs end; in fun global_sublocale expression = gen_global_sublocale (K I) cert_interpretation expression; fun global_sublocale_cmd raw_expression = gen_global_sublocale Locale.check read_interpretation raw_expression; end; (* mixed Isar interface *) local fun register_or_activate lthy = if Named_Target.is_theory lthy then Local_Theory.theory_registration else Locale.add_registration_local_theory; fun gen_isar_interpretation prep_interpretation expression lthy = generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; in fun isar_interpretation expression = gen_isar_interpretation cert_interpretation expression; fun isar_interpretation_cmd raw_expression = gen_isar_interpretation read_interpretation raw_expression; end; end; diff --git a/src/Pure/Isar/named_target.ML b/src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML +++ b/src/Pure/Isar/named_target.ML @@ -1,138 +1,139 @@ (* Title: Pure/Isar/named_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Targets for theory, locale, class -- at the bottom of the nested structure. *) signature NAMED_TARGET = sig val is_theory: local_theory -> bool val locale_of: local_theory -> string option val bottom_locale_of: local_theory -> string option val class_of: local_theory -> string option - val init: string -> theory -> local_theory + val init: string list -> string -> theory -> local_theory val theory_init: theory -> local_theory val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory val reinit: local_theory -> theory -> local_theory end; structure Named_Target: NAMED_TARGET = struct (* context data *) datatype target = Theory | Locale of string | Class of string; fun target_of_ident _ "" = Theory | target_of_ident thy ident = if Locale.defined thy ident then (if Class.is_class thy ident then Class else Locale) ident else error ("No such locale: " ^ quote ident); fun ident_of_target Theory = "" | ident_of_target (Locale locale) = locale | ident_of_target (Class class) = class; fun target_is_theory (SOME Theory) = true | target_is_theory _ = false; fun locale_of_target (SOME (Locale locale)) = SOME locale | locale_of_target (SOME (Class locale)) = SOME locale | locale_of_target _ = NONE; fun class_of_target (SOME (Class class)) = SOME class | class_of_target _ = NONE; structure Data = Proof_Data ( type T = target option; fun init _ = NONE; ); val get_bottom_target = Data.get; fun get_target lthy = if Local_Theory.level lthy = 1 then get_bottom_target lthy else NONE; fun ident_of lthy = case get_target lthy of NONE => error "Not in a named target" | SOME target => ident_of_target target; val is_theory = target_is_theory o get_target; val locale_of = locale_of_target o get_target; val bottom_locale_of = locale_of_target o get_bottom_target; val class_of = class_of_target o get_target; (* operations *) fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun class_foundation class (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); fun operations Theory = {define = Generic_Target.define Generic_Target.theory_target_foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.theory_abbrev, declaration = fn _ => Generic_Target.theory_declaration, theory_registration = Locale.add_registration_theory, locale_dependency = fn _ => error "Not possible in theory target", pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} | operations (Locale locale) = {define = Generic_Target.define (locale_foundation locale), notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), abbrev = Generic_Target.locale_abbrev locale, declaration = Generic_Target.locale_declaration locale, theory_registration = fn _ => error "Not possible in locale target", locale_dependency = Locale.add_dependency locale, pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} | operations (Class class) = {define = Generic_Target.define (class_foundation class), notes = Generic_Target.notes (Generic_Target.locale_target_notes class), abbrev = Class.abbrev class, declaration = Generic_Target.locale_declaration class, theory_registration = fn _ => error "Not possible in class target", locale_dependency = Locale.add_dependency class, pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; fun setup_context Theory = Proof_Context.init_global | setup_context (Locale locale) = Locale.init locale | setup_context (Class class) = Class.init class; -fun init ident thy = +fun init includes ident thy = let val target = target_of_ident thy ident; in thy |> Local_Theory.init {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), - setup = setup_context target #> Data.put (SOME target), + setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes, conclude = I} (operations target) + |> not (null includes) ? Local_Theory.mark_brittle end; -val theory_init = init ""; +val theory_init = init [] ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; -fun reinit lthy = init (ident_of lthy); +fun reinit lthy = init [] (ident_of lthy); end; diff --git a/src/Pure/Isar/parse_spec.ML b/src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML +++ b/src/Pure/Isar/parse_spec.ML @@ -1,180 +1,183 @@ (* Title: Pure/Isar/parse_spec.ML Author: Makarius Parsers for complex specifications. *) signature PARSE_SPEC = sig val thm_name: string -> Attrib.binding parser val opt_thm_name: string -> Attrib.binding parser val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser val simple_spec: (Attrib.binding * string) parser val simple_specs: (Attrib.binding * string list) parser val if_assumes: string list parser val multi_specs: Specification.multi_specs_cmd parser val where_multi_specs: Specification.multi_specs_cmd parser val specification: ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser val constdecl: (binding * string option * mixfix) parser val includes: (xstring * Position.T) list parser val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expression: string list parser val locale_prefix: (string * bool) parser val locale_keyword: string parser val locale_expression: Expression.expression parser val context_element: Element.context parser val statement': (string * string list) list list parser val if_statement': (string * string list) list list parser val statement: (Attrib.binding * (string * string list) list) list parser val if_statement: (Attrib.binding * (string * string list) list) list parser val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser val obtains: Element.obtains parser val long_statement: (Element.context list * Element.statement) parser val long_statement_keyword: string parser val overloaded: bool parser end; structure Parse_Spec: PARSE_SPEC = struct (* simple specifications *) fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s; fun opt_thm_name s = Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s) Binding.empty_atts; val simple_spec = opt_thm_name ":" -- Parse.prop; val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop; val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1); (* structured specifications *) val if_assumes = Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)) []; val multi_specs = Parse.enum1 "|" ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs; val specification = Parse.vars -- where_multi_specs; (* basic constant specifications *) val constdecl = Parse.binding -- (Parse.where_ >> K (NONE, NoSyn) || Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) || Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE)) >> Scan.triple2; (* locale and context elements *) val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position); val locale_fixes = Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix >> (single o Scan.triple1) || Parse.params) >> flat; val locale_insts = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] -- Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []; local val loc_element = Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes || Parse.$$$ "constrains" |-- Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ))) >> Element.Constrains || Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp)) >> Element.Assumes || Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp)) >> Element.Defines || Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.thms1)) >> (curry Element.Notes ""); fun plus1_unless test scan = scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); val instance = Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) -- (Scan.optional (Parse.$$$ "rewrites" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []); in val locale_prefix = Scan.optional (Parse.name -- (Scan.option (Parse.$$$ "?") >> is_none) --| Parse.$$$ ":") ("", false); val locale_keyword = Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || Parse.$$$ "defines" || Parse.$$$ "notes"; -val class_expression = plus1_unless locale_keyword Parse.class; +val locale_keyword' = + Parse.$$$ "includes" || locale_keyword; + +val class_expression = plus1_unless locale_keyword' Parse.class; val locale_expression = let val expr2 = Parse.name_position; val expr1 = locale_prefix -- expr2 -- instance >> (fn ((p, l), i) => (l, (p, i))); - val expr0 = plus1_unless locale_keyword expr1; + val expr0 = plus1_unless locale_keyword' expr1; in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; val context_element = Parse.group (fn () => "context element") loc_element; end; (* statements *) val statement' = Parse.and_list1 (Scan.repeat1 Parse.propp); val if_statement' = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement') []; val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp); val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) []; val cond_statement = Parse.$$$ "if" |-- Parse.!!! statement >> pair true || Parse.$$$ "when" |-- Parse.!!! statement >> pair false || Scan.succeed (true, []); val obtain_case = Parse.parbinding -- (Scan.optional (Parse.and_list1 Parse.vars --| Parse.where_ >> flat) [] -- (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)); val obtains = Parse.enum1 "|" obtain_case; val long_statement = Scan.repeat context_element -- (Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains || Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows); val long_statement_keyword = locale_keyword || Parse.$$$ "obtains" || Parse.$$$ "shows"; (* options *) val overloaded = Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false; end; diff --git a/src/Pure/Isar/target_context.ML b/src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML +++ b/src/Pure/Isar/target_context.ML @@ -1,59 +1,65 @@ (* Title: Pure/Isar/target_context.ML Author: Florian Haftmann Handling of named and nested targets at the Isar toplevel via context begin / end blocks. *) signature TARGET_CONTEXT = sig - val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory + val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T -> + theory -> local_theory val end_named_cmd: local_theory -> Context.generic val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> (local_theory -> Context.generic) * local_theory val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> Context.generic -> local_theory val end_nested_cmd: local_theory -> Context.generic end; structure Target_Context: TARGET_CONTEXT = struct -fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy - | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy; +fun prep_includes thy = + map (Bundle.check (Proof_Context.init_global thy)); + +fun context_begin_named_cmd raw_includes ("-", _) thy = + Named_Target.init (prep_includes thy raw_includes) "" thy + | context_begin_named_cmd raw_includes name thy = + Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy; val end_named_cmd = Context.Theory o Local_Theory.exit_global; fun switch_named_cmd NONE (Context.Theory thy) = - (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy) + (end_named_cmd, Named_Target.theory_init thy) | switch_named_cmd (SOME name) (Context.Theory thy) = - (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy) + (end_named_cmd, context_begin_named_cmd [] name thy) | switch_named_cmd NONE (Context.Proof lthy) = (Context.Proof o Local_Theory.reset, lthy) | switch_named_cmd (SOME name) (Context.Proof lthy) = (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, - (context_begin_named_cmd name o Local_Theory.exit_global_nonbrittle) lthy); + (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy); -fun includes raw_incls lthy = - Bundle.includes (map (Bundle.check lthy) raw_incls) lthy; +fun includes raw_includes lthy = + Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; -fun context_begin_nested_cmd raw_incls raw_elems gthy = +fun context_begin_nested_cmd raw_includes raw_elems gthy = gthy |> Context.cases Named_Target.theory_init Local_Theory.assert - |> includes raw_incls + |> includes raw_includes |> Expression.read_declaration ([], []) I raw_elems |> (#4 o fst) |> Local_Theory.begin_nested |> snd; fun end_nested_cmd lthy = let val lthy' = Local_Theory.end_nested lthy in if Named_Target.is_theory lthy' then Context.Theory (Local_Theory.exit_global lthy') else Context.Proof lthy' end; end; structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end; diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy --- a/src/Pure/Pure.thy +++ b/src/Pure/Pure.thy @@ -1,1504 +1,1510 @@ (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn and "axiomatization" :: thy_stmt and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix" and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "ML_val" "ML_command" :: diag % "ML" and "simproc_setup" :: thy_decl % "ML" and "setup" "local_setup" "attribute_setup" "method_setup" "declaration" "syntax_declaration" "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl_block and "unbundle" :: thy_decl and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block and "interpret" :: prf_goal % "proof" and "interpretation" "global_interpretation" "sublocale" :: thy_goal and "class" :: thy_decl_block and "subclass" :: thy_goal and "instantiation" :: thy_decl_block and "instance" :: thy_goal and "overloading" :: thy_decl_block and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt and "schematic_goal" :: thy_goal_stmt and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" and "show" :: prf_asm_goal % "proof" and "thus" :: prf_asm_goal % "proof" and "then" "from" "with" :: prf_chain % "proof" and "note" :: prf_decl % "proof" and "supply" :: prf_script % "proof" and "using" "unfolding" :: prf_decl % "proof" and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" and "by" ".." "." "sorry" "\" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" and "subgoal" :: prf_script_goal % "proof" and "proof" :: prf_block % "proof" and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" and "help" "print_commands" "print_options" "print_context" "print_theory" "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag and "print_state" :: diag and "welcome" :: diag and "end" :: thy_end and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "\\tag" = "\<^marker>\tag \" and "===>" = "===>" (*prevent replacement of very long arrows*) and "--->" = "\\" and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = "" and "hence" = "then have" and "thus" = "then show" begin section \Isar commands\ subsection \Other files\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files))); val _ = Outer_Syntax.command \<^command_keyword>\bibtex_file\ "check bibtex database file in Prover IDE" (Resources.provide_parse_files "bibtex_file" >> (fn files => Toplevel.theory (fn thy => let val ([{lines, pos, ...}], thy') = files thy; val _ = Bibtex.check_database_output pos (cat_lines lines); in thy' end))); val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" (Parse.path_binding -- (\<^keyword>\=\ |-- Parse.embedded_input) >> Generated_Files.generate_file_cmd); val files_in_theory = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from given theories" (Parse.and_list1 files_in_theory >> (fn args => Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))); val base_dir = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.position Parse.path --| \<^keyword>\)\)) ("", Position.none); val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir; val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false; val executable = \<^keyword>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; val export_files = Scan.repeat1 Parse.path_binding -- executable; val _ = Outer_Syntax.command \<^command_keyword>\compile_generated_files\ "compile generated files and export results" (Parse.and_list files_in_theory -- Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", Position.none) -- (Parse.where_ |-- Parse.!!! Parse.ML_source) >> (fn ((((args, external), export), export_prefix), source) => Toplevel.keep (fn st => Generated_Files.compile_generated_files_cmd (Toplevel.context_of st) args external export export_prefix source))); in end\ subsection \Embedded ML text\ ML \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_export, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); val _ = Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_import, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) end)); val _ = Outer_Syntax.command ("ML_export", \<^here>) "ML text within theory or local theory, and export to bootstrap environment" (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = Outer_Syntax.local_theory \<^command_keyword>\local_setup\ "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" (Parse.range Parse.name -- (\<^keyword>\=\ |-- Parse.ML_source) >> (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); val _ = Outer_Syntax.local_theory \<^command_keyword>\attribute_setup\ "define attribute in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\method_setup\ "define proof method in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" (Parse.name_position -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); in end\ subsection \Theory commands\ subsubsection \Sorts and types\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_synonym\ "declare type abbreviation" (Parse.type_args -- Parse.binding -- (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); in end\ subsubsection \Consts\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ subsubsection \Syntax and translations\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ subsubsection \Translation functions\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); in end\ subsubsection \Specifications\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); val axiomatization = Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.alias_cmd); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.type_alias_cmd); in end\ subsubsection \Notation\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\type_notation\ "add concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_type_notation\ "delete concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\notation\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_notation\ "delete concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); in end\ subsubsection \Theorems\ ML \ local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); val _ = theorem \<^command_keyword>\theorem\ false "theorem"; val _ = theorem \<^command_keyword>\lemma\ false "lemma"; val _ = theorem \<^command_keyword>\corollary\ false "corollary"; val _ = theorem \<^command_keyword>\proposition\ false "proposition"; val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); in end\ subsubsection \Hide names\ ML \ local fun hide_names command_keyword what hide parse prep = Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => (Toplevel.theory (fn thy => let val ctxt = Proof_Context.init_global thy in fold (hide fully o prep ctxt) args thy end)))); val _ = hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of); in end\ subsection \Bundled declarations\ ML \ local val _ = Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\bundle\ "define bundle of declarations" ((Parse.binding --| \<^keyword>\=\) -- Parse.thms1 -- Parse.for_fixes >> (uncurry Bundle.bundle_cmd)) (Parse.binding --| Parse.begin >> Bundle.init); val _ = Outer_Syntax.local_theory \<^command_keyword>\unbundle\ "activate declarations from bundle in local theory" (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd); val _ = Outer_Syntax.command \<^command_keyword>\include\ "activate declarations from bundle in proof body" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\including\ "activate declarations from bundle in goal refinement" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\print_bundles\ "print bundles of declarations" (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); in end\ subsection \Local theory specifications\ subsubsection \Specification context\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\context\ "begin local theory context" ((Parse.name_position - >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) || + >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd [] name)) || Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems))) --| Parse.begin); val _ = Outer_Syntax.command \<^command_keyword>\end\ "end context" (Scan.succeed (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o Toplevel.end_proof (K Proof.end_notepad))); in end\ subsubsection \Locales and interpretation\ ML \ local +val locale_context_elements = + Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element; + val locale_val = Parse_Spec.locale_expression -- - Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || - Scan.repeat1 Parse_Spec.context_element >> pair ([], []); + Scan.optional (\<^keyword>\+\ |-- Parse.!!! locale_context_elements) ([], []) || + locale_context_elements >> pair ([], []); val _ = Outer_Syntax.command \<^command_keyword>\locale\ "define named specification context" (Parse.binding -- - Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin - >> (fn ((name, (expr, elems)), begin) => + Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) (([], []), ([], [])) -- Parse.opt_begin + >> (fn ((name, (expr, (includes, elems))), begin) => Toplevel.begin_main_target begin - (Expression.add_locale_cmd name Binding.empty expr elems #> snd))); + (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\experiment\ "open private specification context" (Scan.repeat Parse_Spec.context_element --| Parse.begin >> (fn elems => Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "prove interpretation of locale expression in proof context" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.proof (Interpretation.interpret_cmd expr))); val interpretation_args_with_defs = Parse.!!! Parse_Spec.locale_expression -- (Scan.optional (\<^keyword>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) ([])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ "prove interpretation of locale expression into global theory" (interpretation_args_with_defs >> (fn (expr, defs) => Interpretation.global_interpretation_cmd expr defs)); val _ = Outer_Syntax.command \<^command_keyword>\sublocale\ "prove sublocale relation between a locale and a locale expression" ((Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\<\) -- interpretation_args_with_defs >> (fn (loc, (expr, defs)) => Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs))) || interpretation_args_with_defs >> (fn (expr, defs) => Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs))); val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "prove interpretation of locale expression in local theory or into global theory" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr))); in end\ subsubsection \Type classes\ ML \ local +val class_context_elements = + Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element; + val class_val = Parse_Spec.class_expression -- - Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || - Scan.repeat1 Parse_Spec.context_element >> pair []; + Scan.optional (\<^keyword>\+\ |-- Parse.!!! class_context_elements) ([], []) || + class_context_elements >> pair []; val _ = Outer_Syntax.command \<^command_keyword>\class\ "define type class" - (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) ([], []) -- Parse.opt_begin - >> (fn ((name, (supclasses, elems)), begin) => + (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) ([], ([], [])) -- Parse.opt_begin + >> (fn ((name, (supclasses, (includes, elems))), begin) => Toplevel.begin_main_target begin - (Class_Declaration.class_cmd name supclasses elems #> snd))); + (Class_Declaration.class_cmd name includes supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\subclass\ "prove a subclass relation" (Parse.class >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command \<^command_keyword>\instantiation\ "instantiate and prove type arity" (Parse.multi_arity --| Parse.begin >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities))); val _ = Outer_Syntax.command \<^command_keyword>\instance\ "prove type arity or subclass relation" ((Parse.class -- ((\<^keyword>\\\ || \<^keyword>\<\) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); in end\ subsubsection \Arbitrary overloading\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\overloading\ "overloaded definitions" (Scan.repeat1 (Parse.name --| (\<^keyword>\==\ || \<^keyword>\\\) -- Parse.term -- Scan.optional (\<^keyword>\(\ |-- (\<^keyword>\unchecked\ >> K false) --| \<^keyword>\)\) true >> Scan.triple1) --| Parse.begin >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations))); in end\ subsection \Proof commands\ ML \ local val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\notepad\ "begin proof context" (Parse.begin >> K Proof.begin_notepad); in end\ subsubsection \Statements\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\have\ "state local goal" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\show\ "state local goal, to refine pending subgoals" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\hence\ "old-style alias of \"then have\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\thus\ "old-style alias of \"then show\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); in end\ subsubsection \Local facts\ ML \ local val facts = Parse.and_list1 Parse.thms1; val _ = Outer_Syntax.command \<^command_keyword>\then\ "forward chaining" (Scan.succeed (Toplevel.proof Proof.chain)); val _ = Outer_Syntax.command \<^command_keyword>\from\ "forward chaining from given facts" (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\with\ "forward chaining from given and current facts" (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\note\ "define facts" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\supply\ "define facts during goal refinement (unstructured)" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\using\ "augment goal facts" (facts >> (Toplevel.proof o Proof.using_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\unfolding\ "unfold definitions in goal and facts" (facts >> (Toplevel.proof o Proof.unfolding_cmd)); in end\ subsubsection \Proof context\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\fix\ "fix local variables (Skolem constants)" (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\assume\ "assume propositions" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\presume\ "assume propositions, to be established later" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\define\ "local definition (non-polymorphic)" ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = Outer_Syntax.command \<^command_keyword>\consider\ "state cases rule" (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\obtain\ "generalized elimination" (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\write\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); val _ = Outer_Syntax.command \<^command_keyword>\case\ "invoke local context" (Parse_Spec.opt_thm_name ":" -- (\<^keyword>\(\ |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding) --| \<^keyword>\)\) || Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); in end\ subsubsection \Proof structure\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\{\ "begin explicit proof block" (Scan.succeed (Toplevel.proof Proof.begin_block)); val _ = Outer_Syntax.command \<^command_keyword>\}\ "end explicit proof block" (Scan.succeed (Toplevel.proof Proof.end_block)); val _ = Outer_Syntax.command \<^command_keyword>\next\ "enter next proof block" (Scan.succeed (Toplevel.proof Proof.next_block)); in end\ subsubsection \End proof\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\qed\ "conclude proof" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command \<^command_keyword>\by\ "terminal backward proof" (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command \<^command_keyword>\..\ "default proof" (Scan.succeed Isar_Cmd.default_proof); val _ = Outer_Syntax.command \<^command_keyword>\.\ "immediate proof" (Scan.succeed Isar_Cmd.immediate_proof); val _ = Outer_Syntax.command \<^command_keyword>\done\ "done proof" (Scan.succeed Isar_Cmd.done_proof); val _ = Outer_Syntax.command \<^command_keyword>\sorry\ "skip proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\\\ "dummy proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\oops\ "forget proof" (Scan.succeed Toplevel.forget_proof); in end\ subsubsection \Proof steps\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\defer\ "shuffle internal proof state" (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); val _ = Outer_Syntax.command \<^command_keyword>\prefer\ "shuffle internal proof state" (Parse.nat >> (Toplevel.proof o Proof.prefer)); val _ = Outer_Syntax.command \<^command_keyword>\apply\ "initial goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); val _ = Outer_Syntax.command \<^command_keyword>\apply_end\ "terminal goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); val _ = Outer_Syntax.command \<^command_keyword>\proof\ "backward proof step" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Toplevel.proof (fn state => let val state' = state |> Proof.proof m |> Seq.the_result ""; val _ = Output.information (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); in state' end)))) in end\ subsubsection \Subgoal focus\ ML \ local val opt_fact_binding = Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) Binding.empty_atts; val for_params = Scan.optional (\<^keyword>\for\ |-- Parse.!!! ((Scan.option Parse.dots >> is_some) -- (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) (false, []); val _ = Outer_Syntax.command \<^command_keyword>\subgoal\ "focus on first subgoal within backward refinement" (opt_fact_binding -- (Scan.option (\<^keyword>\premises\ |-- Parse.!!! opt_fact_binding)) -- for_params >> (fn ((a, b), c) => Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); in end\ subsubsection \Calculation\ ML \ local val calculation_args = Scan.option (\<^keyword>\(\ |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\)\))); val _ = Outer_Syntax.command \<^command_keyword>\also\ "combine calculation and current facts" (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\finally\ "combine calculation and current facts, exhibit result" (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\moreover\ "augment calculation by current facts" (Scan.succeed (Toplevel.proof' Calculation.moreover)); val _ = Outer_Syntax.command \<^command_keyword>\ultimately\ "augment calculation by current facts, exhibit result" (Scan.succeed (Toplevel.proof' Calculation.ultimately)); val _ = Outer_Syntax.command \<^command_keyword>\print_trans_rules\ "print transitivity rules" (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); in end\ subsubsection \Proof navigation\ ML \ local fun report_back () = Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]; val _ = Outer_Syntax.command \<^command_keyword>\back\ "explicit backtracking of proof command" (Scan.succeed (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o Toplevel.skip_proof report_back)); in end\ subsection \Diagnostic commands (for interactive mode only)\ ML \ local val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Outer_Syntax.command \<^command_keyword>\help\ "retrieve outer syntax commands according to name patterns" (Scan.repeat Parse.name >> (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); val _ = Outer_Syntax.command \<^command_keyword>\print_commands\ "print outer syntax commands" (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_options\ "print configuration options" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_context\ "print context of local theory target" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); val _ = Outer_Syntax.command \<^command_keyword>\print_theory\ "print logical theory contents" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_definitions\ "print dependencies of definitional theory content" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_syntax\ "print inner syntax of context" (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_defn_rules\ "print definitional rewrite rules of context" (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_abbrevs\ "print constant abbreviations of context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_theorems\ "print theorems of local theory or proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); val _ = Outer_Syntax.command \<^command_keyword>\print_locales\ "print locales of this theory" (Parse.opt_bang >> (fn verbose => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in Pretty.writeln (Locale.pretty_locales thy verbose) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_classes\ "print classes of this theory" (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ "print interpretations of locale for this theory or proof context" (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\ "print attributes of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_simpset\ "print context of Simplifier" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_rules\ "print intro/elim rules" (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_methods\ "print methods of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ "print ML antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" (Scan.succeed (Toplevel.keep (Toplevel.theory_of #> (fn thy => Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |> Graph_Display.display_graph_old)))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ "print term bindings of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_facts\ "print facts of proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "print cases of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_statement\ "print theorems as long statements" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts); val _ = Outer_Syntax.command \<^command_keyword>\thm\ "print theorems" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms); val _ = Outer_Syntax.command \<^command_keyword>\prf\ "print proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); val _ = Outer_Syntax.command \<^command_keyword>\full_prf\ "print full proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); val _ = Outer_Syntax.command \<^command_keyword>\prop\ "read and print proposition" (opt_modes -- Parse.term >> Isar_Cmd.print_prop); val _ = Outer_Syntax.command \<^command_keyword>\term\ "read and print term" (opt_modes -- Parse.term >> Isar_Cmd.print_term); val _ = Outer_Syntax.command \<^command_keyword>\typ\ "read and print type" (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\::\ |-- Parse.!!! Parse.sort)) >> Isar_Cmd.print_type); val _ = Outer_Syntax.command \<^command_keyword>\print_codesetup\ "print code generator setup" (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_state\ "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); val _ = Outer_Syntax.command \<^command_keyword>\welcome\ "print welcome message" (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); in end\ subsection \Dependencies\ ML \ local val theory_bounds = Parse.theory_name >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\thy_deps\ "visualize theory dependencies" (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); val class_bounds = Parse.sort >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.sort --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\class_deps\ "visualize class dependencies" (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); val _ = Outer_Syntax.command \<^command_keyword>\thm_deps\ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ "print all oracles used in theorems (full graph of transitive dependencies)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; val thms = Attrib.eval_thms ctxt args; in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end))); val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name); val _ = Outer_Syntax.command \<^command_keyword>\unused_thms\ "find unused theorems" (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms_cmd (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ subsubsection \Find consts and theorems\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\find_consts\ "find constants by name / type patterns" (Find_Consts.query_parser >> (fn spec => Toplevel.keep (fn st => Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); val options = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); val _ = Outer_Syntax.command \<^command_keyword>\find_theorems\ "find theorems meeting specified criteria" (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn st => Pretty.writeln (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); in end\ subsection \Code generation\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\code_datatype\ "define set of code datatype constructors" (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); in end\ subsection \Extraction of programs from proofs\ ML \ local val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; val _ = Outer_Syntax.command \<^command_keyword>\realizers\ "specify realizers for primitive axioms / theorems, together with correctness proof" (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command \<^command_keyword>\realizability\ "add equations characterizing realizability" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract_type\ "add equations characterizing type of extracted program" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract\ "extract terms from proofs" (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); in end\ section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ lemma meta_mp: assumes "PROP P \ PROP Q" and "PROP P" shows "PROP Q" by (rule \PROP P \ PROP Q\ [OF \PROP P\]) lemmas meta_impE = meta_mp [elim_format] lemma meta_spec: assumes "\x. PROP P x" shows "PROP P x" by (rule \\x. PROP P x\) lemmas meta_allE = meta_spec [elim_format] lemma swap_params: "(\x y. PROP P x y) \ (\y x. PROP P x y)" .. lemma equal_allI: \(\x. PROP P x) \ (\x. PROP Q x)\ if \\x. PROP P x \ PROP Q x\ by (simp only: that) subsection \Meta-level conjunction\ lemma all_conjunction: "(\x. PROP A x &&& PROP B x) \ ((\x. PROP A x) &&& (\x. PROP B x))" proof assume conj: "\x. PROP A x &&& PROP B x" show "(\x. PROP A x) &&& (\x. PROP B x)" proof - fix x from conj show "PROP A x" by (rule conjunctionD1) from conj show "PROP B x" by (rule conjunctionD2) qed next assume conj: "(\x. PROP A x) &&& (\x. PROP B x)" fix x show "PROP A x &&& PROP B x" proof - show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) qed qed lemma imp_conjunction: "(PROP A \ PROP B &&& PROP C) \ ((PROP A \ PROP B) &&& (PROP A \ PROP C))" proof assume conj: "PROP A \ PROP B &&& PROP C" show "(PROP A \ PROP B) &&& (PROP A \ PROP C)" proof - assume "PROP A" from conj [OF \PROP A\] show "PROP B" by (rule conjunctionD1) from conj [OF \PROP A\] show "PROP C" by (rule conjunctionD2) qed next assume conj: "(PROP A \ PROP B) &&& (PROP A \ PROP C)" assume "PROP A" show "PROP B &&& PROP C" proof - from \PROP A\ show "PROP B" by (rule conj [THEN conjunctionD1]) from \PROP A\ show "PROP C" by (rule conj [THEN conjunctionD2]) qed qed lemma conjunction_imp: "(PROP A &&& PROP B \ PROP C) \ (PROP A \ PROP B \ PROP C)" proof assume r: "PROP A &&& PROP B \ PROP C" assume ab: "PROP A" "PROP B" show "PROP C" proof (rule r) from ab show "PROP A &&& PROP B" . qed next assume r: "PROP A \ PROP B \ PROP C" assume conj: "PROP A &&& PROP B" show "PROP C" proof (rule r) from conj show "PROP A" by (rule conjunctionD1) from conj show "PROP B" by (rule conjunctionD2) qed qed declare [[ML_write_global = false]] end diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,357 +1,356 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash_syntax.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; ML_file "ML/ml_pid.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; +ML_file "Isar/bundle.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; -ML_file "Isar/bundle.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; - ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala.ML"; ML_file "System/scala_compiler.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"