--- a/NEWS Sat Oct 04 22:15:22 2014 +0200
+++ b/NEWS Sat Oct 04 22:15:31 2014 +0200
@@ -38,6 +38,9 @@
*** HOL ***
+* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
+Minor INCOMPATIBILITY.
+
* Bootstrap of listsum as special case of abstract product over lists.
Fact rename:
listsum_def ~> listsum.eq_foldr
--- a/src/Doc/Datatypes/Datatypes.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Sat Oct 04 22:15:31 2014 +0200
@@ -653,9 +653,9 @@
\noindent
In addition, some of the plugins introduce their own constants
-(Section~\ref{sec:plugins}). The case combinator, discriminators, and selectors
-are collectively called \emph{destructors}. The prefix ``@{text "t."}'' is an
-optional component of the names and is normally hidden.
+(Section~\ref{sec:controlling-plugins}). The case combinator, discriminators,
+and selectors are collectively called \emph{destructors}. The prefix
+``@{text "t."}'' is an optional component of the names and is normally hidden.
*}
@@ -685,9 +685,10 @@
\noindent
The full list of named theorems can be obtained as usual by entering the
command \keyw{print_theorems} immediately after the datatype definition.
-This list includes theorems produced by plugins (Section~\ref{sec:plugins}),
-but normally excludes low-level theorems that reveal internal constructions. To
-make these accessible, add the line
+This list includes theorems produced by plugins
+(Section~\ref{sec:controlling-plugins}), but normally excludes low-level
+theorems that reveal internal constructions. To make these accessible, add
+the line
*}
declare [[bnf_note_all]]
@@ -2823,6 +2824,11 @@
\end{description}
\end{indentblock}
+
+In addition, the plugin sets the @{text "[code]"} attribute on a number of
+properties of (co)datatypes and other freely generated types, as documented in
+Sections \ref{ssec:datatype-generated-theorems} and
+\ref{ssec:codatatype-generated-theorems}.
*}
@@ -2852,7 +2858,6 @@
\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
@{thm list.size_o_map[no_vars]}
-(This property is not generated for all datatypes.)
\end{description}
\end{indentblock}
@@ -2925,7 +2930,7 @@
\end{indentblock}
In addition, the plugin sets the @{text "[relator_eq_onp]"} attribute on a
-variant of the @{text t.rel_eq_onp} property generated by the @{text quotient}
+variant of the @{text t.rel_eq_onp} property generated by the @{text lifting}
plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the
@{text "[relator_distr]"} attribute on @{text t.rel_compp}.
*}
--- a/src/Doc/Prog_Prove/Basics.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Sat Oct 04 22:15:31 2014 +0200
@@ -27,7 +27,7 @@
\item[function types,]
denoted by @{text"\<Rightarrow>"}.
\item[type variables,]
- denoted by @{typ 'a}, @{typ 'b}, etc., just like in ML\@.
+ denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@.
\end{description}
Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"},
not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Sat Oct 04 22:15:31 2014 +0200
@@ -94,7 +94,7 @@
\begin{warn}
Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard
arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"},
- @{text"<"} etc) are overloaded: they are available
+ @{text"<"}, etc.) are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
@@ -150,7 +150,7 @@
\subsection{Type \indexed{@{text list}}{list}}
-Although lists are already predefined, we define our own copy just for
+Although lists are already predefined, we define our own copy for
demonstration purposes:
*}
(*<*)
@@ -211,7 +211,7 @@
\begin{figure}[htbp]
\begin{alltt}
\input{MyList.thy}\end{alltt}
-\caption{A Theory of Lists}
+\caption{A theory of lists}
\label{fig:MyList}
\index{comment}
\end{figure}
--- a/src/Doc/Prog_Prove/Isar.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Sat Oct 04 22:15:31 2014 +0200
@@ -73,7 +73,7 @@
Propositions are optionally named formulas. These names can be referred to in
later \isacom{from} clauses. In the simplest case, a fact is such a name.
But facts can also be composed with @{text OF} and @{text of} as shown in
-\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
+\autoref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
that assumptions, intermediate \isacom{have} statements and global lemmas all
have the same status and are thus collectively referred to as
\conceptidx{facts}{fact}.
@@ -217,7 +217,7 @@
Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
-to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.\
+to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.,
thus obviating the need to name them individually.
\section{Proof Patterns}
@@ -863,7 +863,7 @@
Because each \isacom{case} command introduces a list of assumptions
named like the case name, which is the name of a rule of the inductive
definition, those rules now need to be accessed with a qualified name, here
-@{thm[source] ev.ev0} and @{thm[source] ev.evSS}
+@{thm[source] ev.ev0} and @{thm[source] ev.evSS}.
\end{warn}
In the case @{thm[source]evSS} of the proof above we have pretended that the
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Sat Oct 04 22:15:31 2014 +0200
@@ -8,11 +8,11 @@
\section{Type and Function Definitions}
Type synonyms are abbreviations for existing types, for example
-*}
+\index{string@@{text string}}*}
type_synonym string = "char list"
-text{*\index{string@@{text string}}
+text{*
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
\subsection{Datatypes}
@@ -118,7 +118,7 @@
"sq' n \<equiv> n * n"
text{* The key difference is that @{const sq'} is only syntactic sugar:
-after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}, and
+after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}};
before printing, every occurrence of @{term"u*u"} is replaced by
\mbox{@{term"sq' u"}}. Internally, @{const sq'} does not exist.
This is the
@@ -296,7 +296,7 @@
\begin{quote}
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
-Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is
+Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
just not true. The correct generalization is
*};
(*<*)oops;(*>*)
@@ -411,7 +411,7 @@
Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and
@{prop"xs @ [] = xs"}, should be declared as simplification
rules. Equations that may be counterproductive as simplification rules
-should only be used in specific proof steps (see \S\ref{sec:simp} below).
+should only be used in specific proof steps (see \autoref{sec:simp} below).
Distributivity laws, for example, alter the structure of terms
and can produce an exponential blow-up.
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Oct 04 22:15:31 2014 +0200
@@ -6,6 +6,8 @@
theory Code_Test_Scala imports Code_Test begin
+declare [[scala_case_insensitive]]
+
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
value [Scala] "14 + 7 * -12 :: integer"
--- a/src/HOL/Divides.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Divides.thy Sat Oct 04 22:15:31 2014 +0200
@@ -2425,16 +2425,6 @@
subsubsection {* The Divides Relation *}
-lemma dvd_neg_numeral_left [simp]:
- fixes y :: "'a::comm_ring_1"
- shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
- by (fact minus_dvd_iff)
-
-lemma dvd_neg_numeral_right [simp]:
- fixes x :: "'a::comm_ring_1"
- shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
- by (fact dvd_minus_iff)
-
lemmas dvd_eq_mod_eq_0_numeral [simp] =
dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
--- a/src/HOL/Fields.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Fields.thy Sat Oct 04 22:15:31 2014 +0200
@@ -375,6 +375,9 @@
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
by (simp add: field_simps)
+lemma divide_minus1 [simp]: "x / - 1 = - x"
+ using nonzero_minus_divide_right [of "1" x] by simp
+
end
class field_inverse_zero = field +
--- a/src/HOL/Imperative_HOL/Array.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Sat Oct 04 22:15:31 2014 +0200
@@ -255,8 +255,7 @@
lemma effect_nthE [effect_elims]:
assumes "effect (nth a i) h h' r"
obtains "i < length h a" "r = get h a ! i" "h' = h"
- using assms by (rule effectE)
- (erule successE, cases "i < length h a", simp_all add: execute_simps)
+ using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
lemma execute_upd [execute_simps]:
"i < length h a \<Longrightarrow>
@@ -276,8 +275,7 @@
lemma effect_updE [effect_elims]:
assumes "effect (upd i v a) h h' r"
obtains "r = a" "h' = update a i v h" "i < length h a"
- using assms by (rule effectE)
- (erule successE, cases "i < length h a", simp_all add: execute_simps)
+ using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
lemma execute_map_entry [execute_simps]:
"i < length h a \<Longrightarrow>
@@ -298,8 +296,7 @@
lemma effect_map_entryE [effect_elims]:
assumes "effect (map_entry i f a) h h' r"
obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
- using assms by (rule effectE)
- (erule successE, cases "i < length h a", simp_all add: execute_simps)
+ using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
lemma execute_swap [execute_simps]:
"i < length h a \<Longrightarrow>
@@ -320,8 +317,7 @@
lemma effect_swapE [effect_elims]:
assumes "effect (swap i x a) h h' r"
obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
- using assms by (rule effectE)
- (erule successE, cases "i < length h a", simp_all add: execute_simps)
+ using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
lemma execute_freeze [execute_simps]:
"execute (freeze a) h = Some (get h a, h)"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Oct 04 22:15:31 2014 +0200
@@ -82,10 +82,8 @@
lemma successE:
assumes "success f h"
- obtains r h' where "r = fst (the (execute c h))"
- and "h' = snd (the (execute c h))"
- and "execute f h \<noteq> None"
- using assms by (simp add: success_def)
+ obtains r h' where "execute f h = Some (r, h')"
+ using assms by (auto simp: success_def)
named_theorems success_intros "introduction rules for success"
@@ -266,11 +264,11 @@
lemma execute_bind_success:
"success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
- by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
+ by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
lemma success_bind_executeI:
"execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
- by (auto intro!: successI elim!: successE simp add: bind_def)
+ by (auto intro!: successI elim: successE simp add: bind_def)
lemma success_bind_effectI [success_intros]:
"effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
--- a/src/HOL/Int.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Int.thy Sat Oct 04 22:15:31 2014 +0200
@@ -1217,21 +1217,6 @@
divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
- unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
- by simp
-
-lemma half_gt_zero_iff:
- "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
- by auto
-
-lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
-
-lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
- by (fact divide_numeral_1)
-
subsection {* The divides relation *}
--- a/src/HOL/Library/Polynomial.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy Sat Oct 04 22:15:31 2014 +0200
@@ -1724,6 +1724,10 @@
declare gcd_poly.simps [simp del]
+definition lcm_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+where
+ "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)"
+
instance ..
end
--- a/src/HOL/Num.thy Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Num.thy Sat Oct 04 22:15:31 2014 +0200
@@ -1073,6 +1073,22 @@
lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
+subsection {* Particular lemmas concerning @{term 2} *}
+
+context linordered_field_inverse_zero
+begin
+
+lemma half_gt_zero_iff:
+ "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
+ by (auto simp add: field_simps)
+
+lemma half_gt_zero [simp]:
+ "0 < a \<Longrightarrow> 0 < a / 2"
+ by (simp add: half_gt_zero_iff)
+
+end
+
+
subsection {* Numeral equations as default simplification rules *}
declare (in numeral) numeral_One [simp]
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Oct 04 22:15:31 2014 +0200
@@ -1832,8 +1832,7 @@
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
- val fp_eqs =
- map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
+ val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
val killed_As =
map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Oct 04 22:15:31 2014 +0200
@@ -170,8 +170,8 @@
rel_eqs =
let
val ctor_rec_transfers' =
- map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
- val ns' = Integer.sum ns;
+ map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
+ val total_n = Integer.sum ns;
in
HEADGOAL Goal.conjunction_tac THEN
EVERY (map (fn ctor_rec_transfer =>
@@ -187,7 +187,7 @@
REPEAT_DETERM (HEADGOAL
(rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
- HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
+ HEADGOAL (select_prem_tac total_n (dtac asm_rl) (acc + n)) THEN
HEADGOAL (SELECT_GOAL (HEADGOAL
((REPEAT_DETERM o (atac ORELSE'
rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
--- a/src/HOL/Tools/SMT/verit_isar.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML Sat Oct 04 22:15:31 2014 +0200
@@ -50,10 +50,8 @@
name0 :: normalizing_prems ctxt concl0)]
end)
end
- else if rule = veriT_tmp_ite_elim_rule orelse null prems then
- [standard_step Lemma]
else
- [standard_step Plain]
+ [standard_step (if null prems then Lemma else Plain)]
end
in
maps steps_of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Oct 04 22:15:31 2014 +0200
@@ -30,6 +30,7 @@
open ATP_Problem
open ATP_Proof
open ATP_Proof_Reconstruct
+open ATP_Waldmeister
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
@@ -56,7 +57,6 @@
val veriT_simp_arith_rule = "simp_arith"
val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
val veriT_tmp_skolemize_rule = "tmp_skolemize"
-val waldmeister_skolemize_rule = ATP_Waldmeister.waldmeister_skolemize_rule
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
val zipperposition_cnf_rule = "cnf"
@@ -104,8 +104,9 @@
val norm_t = normalize role t
val is_duplicate =
exists (fn (prev_name, prev_role, prev_t, _, _) =>
- member (op =) deps prev_name andalso
- Term.aconv_untyped (normalize prev_role prev_t, norm_t))
+ (prev_role = Hypothesis andalso prev_t aconv t) orelse
+ (member (op =) deps prev_name andalso
+ Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
res
fun looks_boring () = t aconv @{prop False} orelse length deps < 2
@@ -138,7 +139,7 @@
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-fun skolem_methods_of z3 = basic_systematic_methods |> z3 ? cons Moura_Method
+val skolem_methods = Moura_Method :: systematic_methods
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
@@ -186,12 +187,9 @@
fun add_lemma ((l, t), rule) ctxt =
let
val (skos, meths) =
- (if is_skolemize_rule rule then
- (skolems_of ctxt t, skolem_methods_of (rule = z3_skolemize_rule))
- else if is_arith_rule rule then
- ([], arith_methods)
- else
- ([], rewrite_methods))
+ (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
+ else if is_arith_rule rule then ([], arith_methods)
+ else ([], rewrite_methods))
||> massage_methods
in
(Prove ([], skos, l, t, [], ([], []), meths, ""),
@@ -226,6 +224,38 @@
I))))
atp_proof
+ fun is_referenced_in_step _ (Let _) = false
+ | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
+ member (op =) ls l orelse exists (is_referenced_in_proof l) subs
+ and is_referenced_in_proof l (Proof (_, _, steps)) =
+ exists (is_referenced_in_step l) steps
+
+ fun insert_lemma_in_step lem
+ (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
+ let val l' = the (label_of_isar_step lem) in
+ if member (op =) ls l' then
+ [lem, step]
+ else
+ let val refs = map (is_referenced_in_proof l') subs in
+ if length (filter I refs) = 1 then
+ let
+ val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs
+ in
+ [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
+ end
+ else
+ [lem, step]
+ end
+ end
+ and insert_lemma_in_steps lem [] = [lem]
+ | insert_lemma_in_steps lem (step :: steps) =
+ if is_referenced_in_step (the (label_of_isar_step lem)) step then
+ insert_lemma_in_step lem step @ steps
+ else
+ step :: insert_lemma_in_steps lem steps
+ and insert_lemma_in_proof lem (Proof (fix, assms, steps)) =
+ Proof (fix, assms, insert_lemma_in_steps lem steps)
+
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
val finish_off = close_form #> rename_bound_vars
@@ -265,7 +295,7 @@
|> fold add_fact_of_dependencies gamma
|> sort_facts
val meths =
- (if skolem then skolem_methods_of (rule = z3_skolemize_rule)
+ (if skolem then skolem_methods
else if is_arith_rule rule then arith_methods
else if is_datatype_rule rule then datatype_methods
else systematic_methods')
@@ -311,7 +341,7 @@
isar_steps outer (SOME l) (step :: accum) infs
end
and isar_proof outer fix assms lems infs =
- Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
+ Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
val trace = Config.get ctxt trace
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Oct 04 22:15:31 2014 +0200
@@ -710,7 +710,7 @@
name = "ord_frac_simproc", proc = proc3, identifier = []}
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
- @{thm "divide_Numeral1"},
+ @{thm "divide_numeral_1"},
@{thm "divide_zero"}, @{thm divide_zero_left},
@{thm "divide_divide_eq_left"},
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
--- a/src/Tools/Code/code_namespace.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Tools/Code/code_namespace.ML Sat Oct 04 22:15:31 2014 +0200
@@ -6,6 +6,8 @@
signature CODE_NAMESPACE =
sig
+ val variant_case_insensitive: string -> Name.context -> string * Name.context
+
datatype export = Private | Opaque | Public
val is_public: export -> bool
val not_private: export -> bool
@@ -47,6 +49,25 @@
structure Code_Namespace : CODE_NAMESPACE =
struct
+(** name handling on case-insensitive file systems **)
+
+fun restore_for cs =
+ if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper
+ else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper
+ else I;
+
+fun variant_case_insensitive s ctxt =
+ let
+ val cs = Symbol.explode s;
+ val s_lower = implode (map Symbol.to_ascii_lower cs);
+ val restore = implode o restore_for cs o Symbol.explode;
+ in
+ ctxt
+ |> Name.variant s_lower
+ |>> restore
+ end;
+
+
(** export **)
datatype export = Private | Opaque | Public;
--- a/src/Tools/Code/code_scala.ML Sat Oct 04 22:15:22 2014 +0200
+++ b/src/Tools/Code/code_scala.ML Sat Oct 04 22:15:31 2014 +0200
@@ -7,6 +7,7 @@
signature CODE_SCALA =
sig
val target: string
+ val case_insensitive: bool Config.T;
val setup: theory -> theory
end;
@@ -22,6 +23,10 @@
infixr 5 @@;
infixr 5 @|;
+(** preliminary: option to circumvent clashes on case-insensitive file systems **)
+
+val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
+
(** Scala serializer **)
@@ -293,21 +298,24 @@
fun scala_program_of_program ctxt module_name reserved identifiers exports program =
let
+ val variant = if Config.get ctxt case_insensitive
+ then Code_Namespace.variant_case_insensitive
+ else Name.variant;
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
let
val declare = Name.declare name_fragment;
in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
fun namify_class base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_class') = Name.variant base nsp_class
+ val (base', nsp_class') = variant base nsp_class
in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
fun namify_object base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_object') = Name.variant base nsp_object
+ val (base', nsp_object') = variant base nsp_object
in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
fun namify_common base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_common') = Name.variant base nsp_common
+ val (base', nsp_common') = variant base nsp_common
in
(base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
end;