--- a/Admin/Release/CHECKLIST Mon Feb 10 21:50:50 2014 +0100
+++ b/Admin/Release/CHECKLIST Mon Feb 10 21:51:15 2014 +0100
@@ -25,6 +25,10 @@
- check funny base directory, e.g. "Test 中国";
+- check scalable fonts, e.g. src/Doc/ProgProve (NOTE: T1 encoding
+ requires cm-super fonts, which are usually available on MacTeX or
+ Cygwin, but not on Ubuntu/Debian);
+
- diff NEWS wrt. last official release, which is read-only;
- update https://bitbucket.org/isabelle_project/isabelle-release/wiki/Home
--- a/lib/texinputs/isabelle.sty Mon Feb 10 21:50:50 2014 +0100
+++ b/lib/texinputs/isabelle.sty Mon Feb 10 21:51:15 2014 +0100
@@ -197,6 +197,12 @@
\chardef\isacharbackquoteclose=`\`%
}
+\newcommand{\isabellestyleliteralunderscore}{%
+\isabellestyleliteral%
+\def\isacharunderscore{\textunderscore}%
+\def\isacharunderscorekeyword{\textunderscore}%
+}
+
\newcommand{\isabellestylesl}{%
\isabellestyleit%
\def\isastyle{\small\sl}%
--- a/src/Doc/Codegen/Further.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/Codegen/Further.thy Mon Feb 10 21:51:15 2014 +0100
@@ -33,7 +33,7 @@
rather than function definitions are always curried.
The second aspect affects user-defined adaptations with @{command
- code_const}. For regular terms, the @{text Scala} serializer prints
+ code_printing}. For regular terms, the @{text Scala} serializer prints
all type arguments explicitly. For user-defined term adaptations
this is only possible for adaptations which take no arguments: here
the type arguments are just appended. Otherwise they are ignored;
--- a/src/Doc/IsarImplementation/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarImplementation/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage[T1]{fontenc}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{iman,extra,isar,proof}
--- a/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 10 21:51:15 2014 +0100
@@ -2386,13 +2386,7 @@
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
@@ -2494,34 +2488,12 @@
| printing_module ) + '|' )
;
- @@{command (HOL) code_const} (const + @'and') \<newline>
- ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
- ;
-
- @@{command (HOL) code_type} (typeconstructor + @'and') \<newline>
- ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
- ;
-
- @@{command (HOL) code_class} (class + @'and') \<newline>
- ( ( '(' target \<newline> ( @{syntax string} ? + @'and' ) ')' ) + )
- ;
-
- @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \<newline>
- ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
- ;
-
- @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
- ;
-
@@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
| symbol_class | symbol_class_relation | symbol_class_instance
| symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
;
- @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
- ;
-
@@{command (HOL) code_monad} const const target
;
@@ -2629,10 +2601,7 @@
\item @{command (HOL) "code_printing"} associates a series of symbols
(constants, type constructors, classes, class relations, instances,
module names) with target-specific serializations; omitting a serialization
- deletes an existing serialization. Legacy variants of this are
- @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
- @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
- @{command (HOL) "code_include"}.
+ deletes an existing serialization.
\item @{command (HOL) "code_monad"} provides an auxiliary mechanism
to generate monadic code for Haskell.
@@ -2642,8 +2611,6 @@
module names) with target-specific hints how these symbols shall be named.
These hints gain precedence over names for symbols with no hints at all.
Conflicting hints are subject to name disambiguation.
- @{command (HOL) "code_modulename"} is a legacy variant for
- @{command (HOL) "code_identifier"} on module names.
\emph{Warning:} It is at the discretion
of the user to ensure that name prefixes of identifiers in compound
statements like type classes or datatypes are still the same.
--- a/src/Doc/IsarRef/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage{eurosym}
\usepackage[english]{babel}
--- a/src/Doc/IsarRef/document/style.sty Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/document/style.sty Mon Feb 10 21:51:15 2014 +0100
@@ -39,10 +39,10 @@
\parindent 0pt\parskip 0.5ex
-\isabellestyle{literal}
+\isabellestyle{literalunderscore}
\newcommand{\isasymdash}{\isatext{\mbox{-}}}
\railtermfont{\isabellestyle{tt}}
-\railnontermfont{\isabellestyle{literal}}
-\railnamefont{\isabellestyle{literal}}
+\railnontermfont{\isabellestyle{literalunderscore}}
+\railnamefont{\isabellestyle{literalunderscore}}
--- a/src/Doc/System/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/System/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper]{report}
+\usepackage[T1]{fontenc}
\usepackage{supertabular}
\usepackage{graphicx}
\usepackage{iman,extra,isar,ttbox}
--- a/src/HOL/Hoare_Parallel/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Hoare_Parallel/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{report}
\usepackage{graphicx}
\usepackage[english]{babel}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Feb 10 21:51:15 2014 +0100
@@ -575,7 +575,7 @@
text {* Adaption layer *}
-code_include Haskell "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Haskell)
{*import qualified Control.Monad;
import qualified Control.Monad.ST;
import qualified Data.STRef;
@@ -620,7 +620,7 @@
subsubsection {* Scala *}
-code_include Scala "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Scala)
{*object Heap {
def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
}
--- a/src/HOL/MicroJava/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/MicroJava/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-% $Id$
-
-%\documentclass[11pt,a4paper]{article}
\documentclass[11pt,a4paper]{book}
\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
--- a/src/HOL/Number_Theory/Cong.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Mon Feb 10 21:51:15 2014 +0100
@@ -251,10 +251,7 @@
done
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
- apply (subst cong_eq_diff_cong_0_int)
- apply (unfold cong_int_def)
- apply (simp add: dvd_eq_mod_eq_0 [symmetric])
- done
+ by (metis cong_int_def zmod_eq_dvd_iff)
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
by (simp add: cong_altdef_int)
@@ -270,18 +267,11 @@
lemma cong_mult_rcancel_int:
"coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
- apply (subst (1 2) cong_altdef_int)
- apply (subst left_diff_distrib [symmetric])
- apply (rule coprime_dvd_mult_iff_int)
- apply (subst gcd_commute_int, assumption)
- done
+ by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
lemma cong_mult_rcancel_nat:
- assumes "coprime k (m::nat)"
- shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
- apply (rule cong_mult_rcancel_int [transferred])
- using assms apply auto
- done
+ "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+ by (metis cong_mult_rcancel_int [transferred])
lemma cong_mult_lcancel_nat:
"coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
@@ -295,16 +285,12 @@
lemma coprime_cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
\<Longrightarrow> [a = b] (mod m * n)"
- apply (simp only: cong_altdef_int)
- apply (erule (2) divides_mult_int)
- done
+by (metis divides_mult_int cong_altdef_int)
lemma coprime_cong_mult_nat:
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
shows "[a = b] (mod m * n)"
- apply (rule coprime_cong_mult_int [transferred])
- using assms apply auto
- done
+ by (metis assms coprime_cong_mult_int [transferred])
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
@@ -316,61 +302,46 @@
lemma cong_less_unique_nat:
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
- apply auto
- apply (rule_tac x = "a mod m" in exI)
- apply (unfold cong_nat_def, auto)
- done
+ by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
lemma cong_less_unique_int:
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
- apply auto
- apply (rule_tac x = "a mod m" in exI)
- apply (unfold cong_int_def, auto)
- done
+ by (auto simp: cong_int_def) (metis mod_mod_trivial pos_mod_conj)
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
- apply (auto simp add: cong_altdef_int dvd_def field_simps)
+ apply (auto simp add: cong_altdef_int dvd_def)
apply (rule_tac [!] x = "-k" in exI, auto)
done
-lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
- (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
- apply (rule iffI)
- apply (cases "b <= a")
- apply (subst (asm) cong_altdef_nat, assumption)
- apply (unfold dvd_def, auto)
- apply (rule_tac x = k in exI)
- apply (rule_tac x = 0 in exI)
- apply (auto simp add: field_simps)
- apply (subst (asm) cong_sym_eq_nat)
- apply (subst (asm) cong_altdef_nat)
- apply force
- apply (unfold dvd_def, auto)
- apply (rule_tac x = 0 in exI)
- apply (rule_tac x = k in exI)
- apply (auto simp add: field_simps)
- apply (unfold cong_nat_def)
- apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
- apply (erule ssubst)back
- apply (erule subst)
- apply auto
- done
+lemma cong_iff_lin_nat:
+ "([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs")
+proof (rule iffI)
+ assume eqm: ?lhs
+ show ?rhs
+ proof (cases "b \<le> a")
+ case True
+ then show ?rhs using eqm
+ by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult_commute)
+ next
+ case False
+ then show ?rhs using eqm
+ apply (subst (asm) cong_sym_eq_nat)
+ apply (auto simp: cong_altdef_nat)
+ apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
+ done
+ qed
+next
+ assume ?rhs
+ then show ?lhs
+ by (metis cong_nat_def mod_mult_self2 nat_mult_commute)
+qed
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
- apply (subst (asm) cong_iff_lin_int, auto)
- apply (subst add_commute)
- apply (subst (2) gcd_commute_int)
- apply (subst mult_commute)
- apply (subst gcd_add_mult_int)
- apply (rule gcd_commute_int)
- done
+ by (metis cong_int_def gcd_red_int)
lemma cong_gcd_eq_nat:
- assumes "[(a::nat) = b] (mod m)"
- shows "gcd a m = gcd b m"
- apply (rule cong_gcd_eq_int [transferred])
- using assms apply auto
- done
+ "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
+ by (metis assms cong_gcd_eq_int [transferred])
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
by (auto simp add: cong_gcd_eq_nat)
@@ -385,9 +356,7 @@
by (auto simp add: cong_int_def)
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
- apply (subst (1 2) cong_altdef_int)
- apply auto
- done
+ by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
(*
lemma mod_dvd_mod_int:
@@ -460,18 +429,14 @@
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
- apply (simp add: cong_altdef_int)
- apply (subst dvd_minus_iff [symmetric])
- apply (simp add: field_simps)
- done
+ by (metis cong_int_def minus_minus zminus_zmod)
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
by (auto simp add: cong_altdef_int)
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
- apply (cases "b > 0")
- apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
+ apply (cases "b > 0", simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
apply (subst (1 2) cong_modulus_neg_int)
apply (unfold cong_int_def)
apply (subgoal_tac "a * b = (-a * -b)")
@@ -482,11 +447,8 @@
done
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
- apply (cases "a = 0")
- apply force
- apply (subst (asm) cong_altdef_nat)
- apply auto
- done
+ apply (cases "a = 0", force)
+ by (metis cong_altdef_nat leI less_one)
lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)"
unfolding cong_nat_def by auto
@@ -503,40 +465,20 @@
apply auto [1]
apply (drule_tac x = "a - 1" in spec)
apply force
- apply (cases "a = 0")
- apply (metis add_is_0 cong_0_1_nat zero_neq_one)
+ apply (cases "a = 0", simp add: cong_0_1_nat)
apply (rule iffI)
- apply (drule cong_to_1_nat)
- apply (unfold dvd_def)
- apply auto [1]
- apply (rule_tac x = k in exI)
- apply (auto simp add: field_simps) [1]
- apply (subst cong_altdef_nat)
- apply (auto simp add: dvd_def)
+ apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult_commute mult_eq_if)
+ apply (metis cong_add_lcancel_0_nat cong_mult_self_nat)
done
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
- apply (subst cong_altdef_nat)
- apply assumption
- apply (unfold dvd_def, auto simp add: field_simps)
- apply (rule_tac x = k in exI)
- apply auto
- done
+ by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def nat_mult_commute)
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
apply (cases "n = 0")
apply force
apply (frule bezout_nat [of a n], auto)
- apply (rule exI, erule ssubst)
- apply (rule cong_trans_nat)
- apply (rule cong_add_nat)
- apply (subst mult_commute)
- apply (rule cong_mult_self_nat)
- prefer 2
- apply simp
- apply (rule cong_refl_nat)
- apply (rule cong_refl_nat)
- done
+ by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult_commute)
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
apply (cases "n = 0")
@@ -545,18 +487,7 @@
apply (rule_tac x = "-1" in exI)
apply auto
apply (insert bezout_int [of a n], auto)
- apply (rule exI)
- apply (erule subst)
- apply (rule cong_trans_int)
- prefer 2
- apply (rule cong_add_int)
- apply (rule cong_refl_int)
- apply (rule cong_sym_int)
- apply (rule cong_mult_self_int)
- apply simp
- apply (subst mult_commute)
- apply (rule cong_refl_int)
- done
+ by (metis cong_iff_lin_int mult_commute)
lemma cong_solve_dvd_nat:
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
@@ -621,56 +552,34 @@
apply (subst coprime_iff_invertible_nat)
apply auto
apply (auto simp add: cong_nat_def)
- apply (rule_tac x = "x mod m" in exI)
apply (metis mod_less_divisor mod_mult_right_eq)
done
lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
(EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
apply (subst coprime_iff_invertible_int)
- apply auto
apply (auto simp add: cong_int_def)
- apply (rule_tac x = "x mod m" in exI)
- apply (auto simp add: mod_mult_right_eq [symmetric])
+ apply (metis mod_mult_right_eq pos_mod_conj)
done
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
apply (cases "y \<le> x")
- apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
- apply (rule cong_sym_nat)
- apply (subst (asm) (1 2) cong_sym_eq_nat)
- apply (auto simp add: cong_altdef_nat lcm_least_nat)
+ apply (metis cong_altdef_nat lcm_least_nat)
+ apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
done
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
by (auto simp add: cong_altdef_int lcm_least_int) [1]
-lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
- [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) cong_cong_lcm_nat)
- back
- apply (simp add: lcm_nat_def)
- done
-
-lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
- [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) cong_cong_lcm_int)
- back
- apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
- done
-
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (rule cong_cong_coprime_nat)
- apply (subst gcd_commute_nat)
- apply (rule setprod_coprime_nat)
- apply auto
+ apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat)
done
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
@@ -679,10 +588,7 @@
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (rule cong_cong_coprime_int)
- apply (subst gcd_commute_int)
- apply (rule setprod_coprime_int)
- apply auto
+ apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
done
lemma binary_chinese_remainder_aux_nat:
@@ -929,10 +835,7 @@
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (erule (1) coprime_cong_mult_nat)
- apply (subst gcd_commute_nat)
- apply (rule setprod_coprime_nat)
- apply auto
+ apply (metis coprime_cong_mult_nat nat_mult_commute setprod_coprime_nat)
done
lemma chinese_remainder_unique_nat:
--- a/src/HOL/Number_Theory/Pocklington.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy Mon Feb 10 21:51:15 2014 +0100
@@ -668,7 +668,7 @@
subsection{*Prime factorizations*}
-text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
+(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -0,0 +1,28 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Various results of number theory}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+ \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}
+
--- a/src/HOL/ROOT Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/ROOT Mon Feb 10 21:51:15 2014 +0100
@@ -184,6 +184,8 @@
theories
Pocklington
Number_Theory
+ files
+ "document/root.tex"
session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
description {*
--- a/src/HOL/ex/document/root.tex Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/ex/document/root.tex Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage[utf8]{inputenc}
--- a/src/Pure/Isar/code.ML Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Pure/Isar/code.ML Mon Feb 10 21:51:15 2014 +0100
@@ -727,8 +727,9 @@
| Abstract of thm * string
with
-fun dummy_thm thy c =
+fun dummy_thm ctxt c =
let
+ val thy = Proof_Context.theory_of ctxt;
val raw_ty = devarify (const_typ thy c);
val (vs, _) = typscheme thy (c, raw_ty);
val sortargs = case Axclass.class_of_param thy c
@@ -742,11 +743,12 @@
val chead = build_head thy (c, ty);
in Thm.weaken chead Drule.dummy_thm end;
-fun nothing_cert thy c = Nothing (dummy_thm thy c);
+fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
-fun cert_of_eqns thy c [] = Equations (dummy_thm thy c, [])
- | cert_of_eqns thy c raw_eqns =
+fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
+ | cert_of_eqns ctxt c raw_eqns =
let
+ val thy = Proof_Context.theory_of ctxt;
val eqns = burrow_fst (canonize_thms thy) raw_eqns;
val _ = map (assert_eqn thy) eqns;
val (thms, propers) = split_list eqns;
@@ -900,32 +902,38 @@
else Conv.all_conv ct;
in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
-fun rewrite_eqn thy conv ss =
- let
- val ctxt = Proof_Context.init_global thy;
- val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite (put_simpset ss ctxt)));
- in singleton (Variable.trade (K (map rewrite)) ctxt) end;
+fun rewrite_eqn conv ctxt =
+ singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
-fun cert_of_eqns_preprocess thy functrans ss c =
- (map o apfst) (Thm.transfer thy)
- #> perhaps (perhaps_loop (perhaps_apply functrans))
- #> (map o apfst) (rewrite_eqn thy eqn_conv ss)
- #> (map o apfst) (Axclass.unoverload thy)
- #> cert_of_eqns thy c;
+fun preprocess conv ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ in
+ Thm.transfer thy
+ #> rewrite_eqn conv ctxt
+ #> Axclass.unoverload thy
+ end;
+
+fun cert_of_eqns_preprocess ctxt functrans c =
+ perhaps (perhaps_loop (perhaps_apply functrans))
+ #> (map o apfst) (preprocess eqn_conv ctxt)
+ #> cert_of_eqns ctxt c;
fun get_cert thy { functrans, ss } c =
- case retrieve_raw thy c
- of Default (eqns, eqns_lazy) => Lazy.force eqns_lazy
- |> cert_of_eqns_preprocess thy functrans ss c
+ let
+ val ctxt = thy |> Proof_Context.init_global |> put_simpset ss;
+ in
+ case retrieve_raw thy c of
+ Default (_, eqns_lazy) => Lazy.force eqns_lazy
+ |> cert_of_eqns_preprocess ctxt functrans c
| Eqns eqns => eqns
- |> cert_of_eqns_preprocess thy functrans ss c
- | None => nothing_cert thy c
+ |> cert_of_eqns_preprocess ctxt functrans c
+ | None => nothing_cert ctxt c
| Proj (_, tyco) => cert_of_proj thy c tyco
| Abstr (abs_thm, tyco) => abs_thm
- |> Thm.transfer thy
- |> rewrite_eqn thy Conv.arg_conv ss
- |> Axclass.unoverload thy
- |> cert_of_abs thy tyco c;
+ |> preprocess Conv.arg_conv ctxt
+ |> cert_of_abs thy tyco c
+ end;
(* cases *)
--- a/src/Tools/Code/code_haskell.ML Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML Mon Feb 10 21:51:15 2014 +0100
@@ -183,7 +183,7 @@
:: str "="
:: (str o deresolve_const) co
:: print_typ tyvars BR ty
- :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
+ :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
)
end
| print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
@@ -201,7 +201,7 @@
:: str "="
:: print_co co
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
- @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
+ @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
)
end
| print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
@@ -227,37 +227,38 @@
| print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun requires_args classparam = case const_syntax classparam
- of NONE => NONE
- | SOME (_, Code_Printer.Plain_printer _) => SOME 0
- | SOME (k, Code_Printer.Complex_printer _) => SOME k;
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
- case requires_args classparam
- of NONE => semicolon [
- (str o Long_Name.base_name o deresolve_const) classparam,
+ case const_syntax classparam of
+ NONE => semicolon [
+ (str o Long_Name.base_name o deresolve_const) classparam,
+ str "=",
+ print_app tyvars (SOME thm) reserved NOBR (const, [])
+ ]
+ | SOME (_, Code_Printer.Plain_printer s) => semicolon [
+ (str o Long_Name.base_name) s,
+ str "=",
+ print_app tyvars (SOME thm) reserved NOBR (const, [])
+ ]
+ | SOME (k, Code_Printer.Complex_printer _) =>
+ let
+ val { sym = Constant c, dom, range, ... } = const;
+ val (vs, rhs) = (apfst o map) fst
+ (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+ val s = if (is_some o const_syntax) c
+ then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
+ val vars = reserved
+ |> intro_vars (map_filter I (s :: vs));
+ val lhs = IConst { sym = Constant classparam, typargs = [],
+ dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
+ (*dictionaries are not relevant at this late stage,
+ and these consts never need type annotations for disambiguation *)
+ in
+ semicolon [
+ print_term tyvars (SOME thm) vars NOBR lhs,
str "=",
- print_app tyvars (SOME thm) reserved NOBR (const, [])
+ print_term tyvars (SOME thm) vars NOBR rhs
]
- | SOME k =>
- let
- val { sym = Constant c, dom, range, ... } = const;
- val (vs, rhs) = (apfst o map) fst
- (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
- val s = if (is_some o const_syntax) c
- then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
- val vars = reserved
- |> intro_vars (map_filter I (s :: vs));
- val lhs = IConst { sym = Constant classparam, typargs = [],
- dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
- (*dictionaries are not relevant at this late stage,
- and these consts never need type annotations for disambiguation *)
- in
- semicolon [
- print_term tyvars (SOME thm) vars NOBR lhs,
- str "=",
- print_term tyvars (SOME thm) vars NOBR rhs
- ]
- end;
+ end;
in
Pretty.block_enclose (
Pretty.block [
--- a/src/Tools/Code/code_preproc.ML Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon Feb 10 21:51:15 2014 +0100
@@ -264,15 +264,16 @@
(* retrieving equations and instances from the background context *)
-fun obtain_eqns thy eqngr c =
+fun obtain_eqns ctxt eqngr c =
case try (Graph.get_node eqngr) c
of SOME (lhs, cert) => ((lhs, []), cert)
| NONE => let
+ val thy = Proof_Context.theory_of ctxt;
val functrans = (map (fn (_, (_, f)) => f thy)
o #functrans o the_thmproc) thy;
- val {pre, ...} = the_thmproc thy;
- val cert = Code.get_cert thy { functrans = functrans, ss = pre } c;
- val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
+ val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
+ val (lhs, rhss) =
+ Code.typargs_deps_of_cert thy cert;
in ((lhs, rhss), cert) end;
fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -289,7 +290,7 @@
(* computing instantiations *)
-fun add_classes thy arities eqngr c_k new_classes vardeps_data =
+fun add_classes ctxt arities eqngr c_k new_classes vardeps_data =
let
val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
val diff_classes = new_classes |> subtract (op =) old_classes;
@@ -299,82 +300,82 @@
in
vardeps_data
|> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
- |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
- |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
+ |> fold (fn styp => fold (ensure_typmatch_inst ctxt arities eqngr styp) new_classes) styps
+ |> fold (fn c_k => add_classes ctxt arities eqngr c_k diff_classes) c_ks
end end
-and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
+and add_styp ctxt arities eqngr c_k new_tyco_styps vardeps_data =
let
val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
else
vardeps_data
|> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
- |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
+ |> fold (ensure_typmatch_inst ctxt arities eqngr new_tyco_styps) classes
end
-and add_dep thy arities eqngr c_k c_k' vardeps_data =
+and add_dep ctxt arities eqngr c_k c_k' vardeps_data =
let
val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
in
vardeps_data
- |> add_classes thy arities eqngr c_k' classes
+ |> add_classes ctxt arities eqngr c_k' classes
|> apfst (Vargraph.add_edge (c_k, c_k'))
end
-and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
- if can (Sign.arity_sorts thy tyco) [class]
+and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
+ if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
then vardeps_data
- |> ensure_inst thy arities eqngr (class, tyco)
+ |> ensure_inst ctxt arities eqngr (class, tyco)
|> fold_index (fn (k, styp) =>
- ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+ ensure_typmatch ctxt arities eqngr styp (Inst (class, tyco), k)) styps
else vardeps_data (*permissive!*)
-and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+and ensure_inst ctxt arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
if member (op =) insts inst then vardeps_data
else let
val (classess, (super_classes, inst_params)) =
- obtain_instance thy arities inst;
+ obtain_instance (Proof_Context.theory_of ctxt) arities inst;
in
vardeps_data
|> (apsnd o apsnd) (insert (op =) inst)
|> fold_index (fn (k, _) =>
apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
- |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
- |> fold (ensure_fun thy arities eqngr) inst_params
+ |> fold (fn super_class => ensure_inst ctxt arities eqngr (super_class, tyco)) super_classes
+ |> fold (ensure_fun ctxt arities eqngr) inst_params
|> fold_index (fn (k, classes) =>
- add_classes thy arities eqngr (Inst (class, tyco), k) classes
+ add_classes ctxt arities eqngr (Inst (class, tyco), k) classes
#> fold (fn super_class =>
- add_dep thy arities eqngr (Inst (super_class, tyco), k)
+ add_dep ctxt arities eqngr (Inst (super_class, tyco), k)
(Inst (class, tyco), k)) super_classes
#> fold (fn inst_param =>
- add_dep thy arities eqngr (Fun inst_param, k)
+ add_dep ctxt arities eqngr (Fun inst_param, k)
(Inst (class, tyco), k)
) inst_params
) classess
end
-and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+and ensure_typmatch ctxt arities eqngr (Tyco tyco_styps) c_k vardeps_data =
vardeps_data
- |> add_styp thy arities eqngr c_k tyco_styps
- | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+ |> add_styp ctxt arities eqngr c_k tyco_styps
+ | ensure_typmatch ctxt arities eqngr (Var c_k') c_k vardeps_data =
vardeps_data
- |> add_dep thy arities eqngr c_k c_k'
- | ensure_typmatch thy arities eqngr Free c_k vardeps_data =
+ |> add_dep ctxt arities eqngr c_k c_k'
+ | ensure_typmatch ctxt arities eqngr Free c_k vardeps_data =
vardeps_data
-and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
+and ensure_rhs ctxt arities eqngr (c', styps) vardeps_data =
vardeps_data
- |> ensure_fun thy arities eqngr c'
+ |> ensure_fun ctxt arities eqngr c'
|> fold_index (fn (k, styp) =>
- ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
-and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+ ensure_typmatch ctxt arities eqngr styp (Fun c', k)) styps
+and ensure_fun ctxt arities eqngr c (vardeps_data as (_, (eqntab, _))) =
if Symtab.defined eqntab c then vardeps_data
else let
- val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
+ val ((lhs, rhss), eqns) = obtain_eqns ctxt eqngr c;
val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
in
vardeps_data
|> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
|> fold_index (fn (k, _) =>
apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
- |> fold_index (fn (k, (_, sort)) =>
- add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
- |> fold (ensure_rhs thy arities eqngr) rhss'
+ |> fold_index (fn (k, (_, sort)) => add_classes ctxt arities eqngr (Fun c, k)
+ (complete_proper_sort (Proof_Context.theory_of ctxt) sort)) lhs
+ |> fold (ensure_rhs ctxt arities eqngr) rhss'
end;
@@ -413,11 +414,13 @@
fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
let
+ val {pre, ...} = the_thmproc thy;
+ val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
val (vardeps, (eqntab, insts)) = empty_vardeps_data
- |> fold (ensure_fun thy arities eqngr) cs
- |> fold (ensure_rhs thy arities eqngr) cs_rhss;
+ |> fold (ensure_fun ctxt arities eqngr) cs
+ |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
val arities' = fold (add_arity thy vardeps) insts arities;
val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
--- a/src/Tools/Code/code_target.ML Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_target.ML Mon Feb 10 21:51:15 2014 +0100
@@ -53,16 +53,9 @@
type identifier_data
val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
-> theory -> theory
- type raw_const_syntax = Code_Printer.raw_const_syntax
- type tyco_syntax = Code_Printer.tyco_syntax
- val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
+ val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
-> theory -> theory
- val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
- val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
- val add_class_syntax: string -> class -> string option -> theory -> theory
- val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
- val add_include: string -> string * (string * string list) option -> theory -> theory
val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
@@ -584,15 +577,6 @@
val set_identifiers = gen_set_identifiers cert_name_decls;
val set_identifiers_cmd = gen_set_identifiers read_name_decls;
-fun add_module_alias_cmd target aliasses thy =
- let
- val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
- in
- fold (fn (sym, name) => set_identifier
- (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
- aliasses thy
- end;
-
(* custom printings *)
@@ -620,62 +604,9 @@
val set_printings = gen_set_printings cert_printings;
val set_printings_cmd = gen_set_printings read_printings;
-fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
- let
- val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
- val x = prep_x thy raw_x;
- in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
-
-fun gen_add_const_syntax prep_const =
- gen_add_syntax Constant prep_const check_const_syntax;
-
-fun gen_add_tyco_syntax prep_tyco =
- gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
-
-fun gen_add_class_syntax prep_class =
- gen_add_syntax Type_Class prep_class ((K o K o K) I);
-
-fun gen_add_instance_syntax prep_inst =
- gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
-
-fun gen_add_include prep_const target (name, some_content) thy =
- gen_add_syntax Module (K I)
- (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
- target name some_content thy;
-
(* concrete syntax *)
-local
-
-fun zip_list (x :: xs) f g =
- f
- :|-- (fn y =>
- fold_map (fn x => g |-- f >> pair x) xs
- :|-- (fn xys => pair ((x, y) :: xys)));
-
-fun process_multi_syntax parse_thing parse_syntax change =
- (Parse.and_list1 parse_thing
- :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
- (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
- >> (Toplevel.theory oo fold)
- (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
-
-in
-
-val add_reserved = add_reserved;
-val add_const_syntax = gen_add_const_syntax (K I);
-val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
-val add_class_syntax = gen_add_class_syntax cert_class;
-val add_instance_syntax = gen_add_instance_syntax cert_inst;
-val add_include = gen_add_include (K I);
-
-val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
-val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
-val add_class_syntax_cmd = gen_add_class_syntax read_class;
-val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
-val add_include_cmd = gen_add_include Code.read_const;
-
fun parse_args f args =
case Scan.read Token.stopper f args
of SOME x => x
@@ -736,11 +667,6 @@
>> (Toplevel.theory o fold set_identifiers_cmd));
val _ =
- Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
- (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
- >> (fn (target, modlnames) => (Toplevel.theory o add_module_alias_cmd target) modlnames));
-
-val _ =
Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
@@ -748,40 +674,9 @@
>> (Toplevel.theory o fold set_printings_cmd));
val _ =
- Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
- (process_multi_syntax Parse.term Code_Printer.parse_const_syntax
- add_const_syntax_cmd);
-
-val _ =
- Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
- (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax
- add_tyco_syntax_cmd);
-
-val _ =
- Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
- (process_multi_syntax Parse.class Parse.string
- add_class_syntax_cmd);
-
-val _ =
- Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
- (process_multi_syntax parse_inst_ident (Parse.minus >> K ())
- add_instance_syntax_cmd);
-
-val _ =
- Outer_Syntax.command @{command_spec "code_include"}
- "declare piece of code to be included in generated code"
- (Parse.name -- Parse.name -- (Parse.text :|--
- (fn "-" => Scan.succeed NONE
- | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
- >> (fn ((target, name), content_consts) =>
- (Toplevel.theory o add_include_cmd target) (name, content_consts)));
-
-val _ =
Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
(Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
-end; (*local*)
-
(** external entrance point -- for codegen tool **)
--- a/src/Tools/Code_Generator.thy Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code_Generator.thy Mon Feb 10 21:51:15 2014 +0100
@@ -8,8 +8,7 @@
imports Pure
keywords
"value" "print_codeproc" "code_thms" "code_deps" :: diag and
- "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
- "code_const" "code_reserved" "code_include" "code_modulename"
+ "export_code" "code_identifier" "code_printing" "code_reserved"
"code_monad" "code_reflect" :: thy_decl and
"datatypes" "functions" "module_name" "file" "checking"
"constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"