# HG changeset patch # User wenzelm # Date 1412453731 -7200 # Node ID 48e23e34241517106c05736794ec6dbad12391c9 # Parent 872f330a0f8a0b8bcf5e867ceac68c066a2556f3# Parent ad010811f45053ea333b33fe58e9992058e3df16 merged; diff -r 872f330a0f8a -r 48e23e342415 NEWS --- 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 diff -r 872f330a0f8a -r 48e23e342415 src/Doc/Datatypes/Datatypes.thy --- 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}. *} diff -r 872f330a0f8a -r 48e23e342415 src/Doc/Prog_Prove/Basics.thy --- 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"\"}. \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 \ 'b list"} means @{typ[source]"'a \ ('b list)"}, not @{typ"('a \ 'b) list"}: postfix type constructors have precedence diff -r 872f330a0f8a -r 48e23e342415 src/Doc/Prog_Prove/Bool_nat_list.thy --- 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"\"}, - @{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} diff -r 872f330a0f8a -r 48e23e342415 src/Doc/Prog_Prove/Isar.thy --- 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 diff -r 872f330a0f8a -r 48e23e342415 src/Doc/Prog_Prove/Types_and_funs.thy --- 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 \ 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. diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- 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" diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Divides.thy --- 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 \ (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) \ 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 diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Fields.thy --- 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 \ 0 \ z \ 0 \ (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 + diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Imperative_HOL/Array.thy --- 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 \ @@ -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 \ @@ -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 \ @@ -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)" diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ 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 \ execute (f \= 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') \ success (g x) h' \ success (f \= 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 \ success (g x) h' \ success (f \= g) h" diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Int.thy --- 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 *} diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Library/Polynomial.thy --- 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 \ 'a poly \ 'a poly" +where + "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)" + instance .. end diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Num.thy --- 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 \ 0 < a" (is "?P \ ?Q") + by (auto simp add: field_simps) + +lemma half_gt_zero [simp]: + "0 < a \ 0 < a / 2" + by (simp add: half_gt_zero_iff) + +end + + subsection {* Numeral equations as default simplification rules *} declare (in numeral) numeral_One [simp] diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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) diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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' diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Tools/SMT/verit_isar.ML --- 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 diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 872f330a0f8a -r 48e23e342415 src/HOL/Tools/numeral_simprocs.ML --- 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"}, diff -r 872f330a0f8a -r 48e23e342415 src/Tools/Code/code_namespace.ML --- 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; diff -r 872f330a0f8a -r 48e23e342415 src/Tools/Code/code_scala.ML --- 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;