--- a/src/HOL/Code_Numeral.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Code_Numeral.thy Sat Dec 19 23:19:10 2015 +0100
@@ -648,6 +648,12 @@
and (Haskell) infix 4 "<"
and (Scala) infixl 4 "<"
and (Eval) infixl 6 "<"
+| constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
+ (SML) "IntInf.abs"
+ and (OCaml) "Big'_int.abs'_big'_int"
+ and (Haskell) "Prelude.abs"
+ and (Scala) "_.abs"
+ and (Eval) "abs"
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat Dec 19 23:19:10 2015 +0100
@@ -4,10 +4,20 @@
Test case for test_code on GHC
*)
-theory Code_Test_GHC imports "../Library/Code_Test" begin
+theory Code_Test_GHC imports "../Library/Code_Test" "../GCD" begin
test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
value [GHC] "14 + 7 * -12 :: integer"
+test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+ "gcd 15 10 = (5 :: integer)"
+ "gcd 15 (- 10) = (5 :: integer)"
+ "gcd (- 10) 15 = (5 :: integer)"
+ "gcd (- 10) (- 15) = (5 :: integer)"
+ "gcd 0 (- 10) = (10 :: integer)"
+ "gcd (- 10) 0 = (10 :: integer)"
+ "gcd 0 0 = (0 :: integer)"
+in GHC
+
end
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat Dec 19 23:19:10 2015 +0100
@@ -4,10 +4,20 @@
Test case for test_code on OCaml
*)
-theory Code_Test_OCaml imports "../Library/Code_Test" begin
+theory Code_Test_OCaml imports "../Library/Code_Test" "../GCD" begin
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
value [OCaml] "14 + 7 * -12 :: integer"
+test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+ "gcd 15 10 = (5 :: integer)"
+ "gcd 15 (- 10) = (5 :: integer)"
+ "gcd (- 10) 15 = (5 :: integer)"
+ "gcd (- 10) (- 15) = (5 :: integer)"
+ "gcd 0 (- 10) = (10 :: integer)"
+ "gcd (- 10) 0 = (10 :: integer)"
+ "gcd 0 0 = (0 :: integer)"
+in OCaml
+
end
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat Dec 19 23:19:10 2015 +0100
@@ -4,7 +4,7 @@
Test case for test_code on Scala
*)
-theory Code_Test_Scala imports "../Library/Code_Test" begin
+theory Code_Test_Scala imports "../Library/Code_Test" "../GCD" begin
declare [[scala_case_insensitive]]
@@ -12,4 +12,14 @@
value [Scala] "14 + 7 * -12 :: integer"
+test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+ "gcd 15 10 = (5 :: integer)"
+ "gcd 15 (- 10) = (5 :: integer)"
+ "gcd (- 10) 15 = (5 :: integer)"
+ "gcd (- 10) (- 15) = (5 :: integer)"
+ "gcd 0 (- 10) = (10 :: integer)"
+ "gcd (- 10) 0 = (10 :: integer)"
+ "gcd 0 0 = (0 :: integer)"
+in Scala
+
end
--- a/src/HOL/GCD.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/GCD.thy Sat Dec 19 23:19:10 2015 +0100
@@ -2196,4 +2196,33 @@
lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
and Gcd_insert_int = Gcd_insert [where ?'a = int]
+subsection \<open>gcd and lcm instances for @{typ integer}\<close>
+
+instantiation integer :: gcd begin
+context includes integer.lifting begin
+lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
+lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
end
+instance ..
+end
+lifting_update integer.lifting
+lifting_forget integer.lifting
+
+context includes integer.lifting begin
+
+lemma gcd_code_integer [code]:
+ "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+by transfer(fact gcd_code_int)
+
+lemma lcm_code_integer [code]: "lcm (a::integer) b = (abs a) * (abs b) div gcd a b"
+by transfer(fact lcm_altdef_int)
+
+end
+
+code_printing constant "gcd :: integer \<Rightarrow> _"
+ \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
+ and (Haskell) "Prelude.gcd"
+ and (Scala) "_.gcd'((_)')"
+ -- \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
+
+end
--- a/src/HOL/Hilbert_Choice.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sat Dec 19 23:19:10 2015 +0100
@@ -6,7 +6,7 @@
section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
theory Hilbert_Choice
-imports Nat Wellfounded
+imports Wellfounded
keywords "specification" :: thy_goal
begin
--- a/src/HOL/Library/Code_Target_Int.thy Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Sat Dec 19 23:19:10 2015 +0100
@@ -5,7 +5,7 @@
section \<open>Implementation of integer numbers by target-language integers\<close>
theory Code_Target_Int
-imports Main
+imports "../GCD"
begin
code_datatype int_of_integer
@@ -94,6 +94,15 @@
lemma [code]:
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
by transfer rule
+
+lemma gcd_int_of_integer [code]:
+ "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
+by transfer rule
+
+lemma lcm_int_of_integer [code]:
+ "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
+by transfer rule
+
end
lemma (in ring_1) of_int_code_if:
--- a/src/HOL/TPTP/atp_problem_import.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Sat Dec 19 23:19:10 2015 +0100
@@ -315,6 +315,7 @@
| "DFG" => (DFG Monomorphic, "mono_native", liftingN)
| _ => error ("Unknown format " ^ quote format_str ^
" (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
+ val generate_info = false
val uncurried_aliases = false
val readable_names = true
val presimp = true
@@ -322,7 +323,8 @@
map (apfst (rpair (Global, Non_Rec_Def))) defs @
map (apfst (rpair (Global, General))) nondefs
val (atp_problem, _, _, _) =
- generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
+ generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
+ Translator
lam_trans uncurried_aliases readable_names presimp [] conj facts
val ord = effective_term_order ctxt spassN
--- a/src/HOL/TPTP/atp_theory_export.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Sat Dec 19 23:19:10 2015 +0100
@@ -75,12 +75,11 @@
| SOME failure => string_of_atp_failure failure))
in outcome end
-fun is_problem_line_reprovable ctxt format prelude axioms deps
- (Formula (ident', _, phi, _, _)) =
+fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) =
is_none (run_atp ctxt format
- ((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
- map_filter (Symtab.lookup axioms) deps) ::
- prelude))
+ ((factsN,
+ Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) ::
+ prelude))
| is_problem_line_reprovable _ _ _ _ _ _ = false
fun inference_term _ [] = NONE
@@ -93,7 +92,7 @@
|> SOME
fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
- (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
+ (line as Formula ((ident, alt), Axiom, phi, NONE, info)) =
let
val deps =
case these (AList.lookup (op =) infers ident) of
@@ -106,7 +105,7 @@
else
deps
in
- Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
+ Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info)
end
| add_inferences_to_problem_line _ _ _ _ _ _ line = line
@@ -170,7 +169,7 @@
facts
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
- |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
+ |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
@{prop False}
|> #1 |> sort_by (heading_sort_key o fst)
val prelude = fst (split_last problem)
@@ -269,13 +268,13 @@
val hol_base_name = encode_meta "HOL"
fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
- case try (Global_Theory.get_thm thy) alt of
+ (case try (Global_Theory.get_thm thy) alt of
SOME th =>
- (* This is a crude hack to detect theorems stated and proved by the user (as
- opposed to those derived by various packages). In addition, we leave out
- everything in "HOL" as too basic to be interesting. *)
+ (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those
+ derived by various packages). In addition, we leave out everything in "HOL" as too basic to
+ be interesting. *)
Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
- | NONE => false
+ | NONE => false)
(* Convention: theoryname__goalname *)
fun problem_name_of base_name n alt =
@@ -342,13 +341,12 @@
| write_problem_files n seen_facts includes seen_ss
((base_name, fact_line :: fact_lines) :: groups) =
let
- val (ident, alt, pname, sname, conj) =
+ val (alt, pname, sname, conj) =
(case fact_line of
Formula ((ident, alt), _, phi, _, _) =>
- (ident, alt, problem_name_of base_name n (encode_meta alt),
+ (alt, problem_name_of base_name n (encode_meta alt),
suggestion_name_of base_name n (encode_meta alt),
Formula ((ident, alt), Conjecture, phi, NONE, [])))
-
val fact = the (Symtab.lookup fact_tab alt)
val fact_s = tptp_string_of_line format fact_line
in
--- a/src/HOL/Tools/ATP/atp_problem.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Dec 19 23:19:10 2015 +0100
@@ -98,7 +98,7 @@
val tptp_empty_list : string
val dfg_individual_type : string
val isabelle_info_prefix : string
- val isabelle_info : string -> int -> (string, 'a) atp_term list
+ val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
val extract_isabelle_status : (string, 'a) atp_term list -> string option
val extract_isabelle_rank : (string, 'a) atp_term list -> int
val inductionN : string
@@ -138,6 +138,7 @@
('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
val is_format_higher_order : atp_format -> bool
+ val tptp_string_of_format : atp_format -> string
val tptp_string_of_line : atp_format -> string atp_problem_line -> string
val lines_of_atp_problem :
atp_format -> term_order -> (unit -> (string * int) list)
@@ -271,12 +272,16 @@
val default_rank = 1000
val default_term_order_weight = 1
-(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
-fun isabelle_info status rank =
- [] |> rank <> default_rank
- ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
- [ATerm ((string_of_int rank, []), [])]))
- |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
+(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle
+ metainformation. *)
+fun isabelle_info generate_info status rank =
+ if generate_info then
+ [] |> rank <> default_rank
+ ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
+ [ATerm ((string_of_int rank, []), [])]))
+ |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
+ else
+ []
fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
try (unprefix isabelle_info_prefix) s
@@ -542,13 +547,16 @@
| tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
" : " ^ string_of_type format ty ^ ").\n"
- | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) =
+ | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) =
tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
tptp_string_of_role kind ^ "," ^ "\n (" ^
tptp_string_of_formula format phi ^ ")" ^
(case source of
SOME tm => ", " ^ tptp_string_of_term format tm
- | NONE => "") ^
+ | NONE => if null info then "" else ", []") ^
+ (case info of
+ [] => ""
+ | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^
")." ^ maybe_alt alt ^ "\n"
fun tptp_lines format =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Dec 19 23:19:10 2015 +0100
@@ -112,9 +112,10 @@
Proof.context -> type_enc -> string -> term list -> term list * term list
val string_of_status : status -> string
val factsN : string
- val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
- string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
- string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
+ val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc ->
+ mode -> string -> bool -> bool -> bool -> term list -> term ->
+ ((string * stature) * term) list -> string atp_problem * string Symtab.table
+ * (string * term) list * int Symtab.table
val atp_problem_selection_weights : string atp_problem -> (string * real) list
val atp_problem_term_order_info : string atp_problem -> (string * int) list
end;
@@ -2017,7 +2018,7 @@
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP forbids name clashes, and some of the remote
provers might care. *)
-fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
+fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank
(j, {name, stature = (_, status), role, iformula, atomic_types}) =
Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
encode name, alt name),
@@ -2027,23 +2028,22 @@
should_guard_var_in_formula (if pos then SOME true else NONE)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
- NONE, isabelle_info (string_of_status status) (rank j))
+ NONE, isabelle_info generate_info (string_of_status status) (rank j))
-fun lines_of_subclass type_enc sub super =
+fun lines_of_subclass generate_info type_enc sub super =
Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
AConn (AImplies,
[sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
|> bound_tvars type_enc false [tvar_a],
- NONE, isabelle_info inductiveN helper_rank)
+ NONE, isabelle_info generate_info inductiveN helper_rank)
-fun lines_of_subclass_pair type_enc (sub, supers) =
+fun lines_of_subclass_pair generate_info type_enc (sub, supers) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
- [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
- map (`make_class) supers)]
+ [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)]
else
- map (lines_of_subclass type_enc sub) supers
+ map (lines_of_subclass generate_info type_enc sub) supers
-fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
+fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
Class_Memb (class_memb_prefix ^ name,
map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
@@ -2053,14 +2053,12 @@
mk_ahorn (maps (class_atoms type_enc) prems)
(class_atom type_enc (cl, T))
|> bound_tvars type_enc true (snd (dest_Type T)),
- NONE, isabelle_info inductiveN helper_rank)
+ NONE, isabelle_info generate_info inductiveN helper_rank)
-fun line_of_conjecture ctxt mono type_enc
- ({name, role, iformula, atomic_types, ...} : ifact) =
+fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
Formula ((conjecture_prefix ^ name, ""), role,
iformula
- |> formula_of_iformula ctxt mono type_enc
- should_guard_var_in_formula (SOME false)
+ |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
@@ -2230,7 +2228,7 @@
? fold (add_fact_monotonic_types ctxt mono type_enc) facts
end
-fun line_of_guards_mono_type ctxt mono type_enc T =
+fun line_of_guards_mono_type ctxt generate_info mono type_enc T =
Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
Axiom,
IConst (`make_bound_var "X", T, [])
@@ -2240,21 +2238,21 @@
(SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
- NONE, isabelle_info inductiveN helper_rank)
+ NONE, isabelle_info generate_info inductiveN helper_rank)
-fun line_of_tags_mono_type ctxt mono type_enc T =
+fun line_of_tags_mono_type ctxt generate_info mono type_enc T =
let val x_var = ATerm ((`make_bound_var "X", []), []) in
Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
eq_formula type_enc (atomic_types_of T) [] false
(tag_with_type ctxt mono type_enc NONE T x_var) x_var,
- NONE, isabelle_info non_rec_defN helper_rank)
+ NONE, isabelle_info generate_info non_rec_defN helper_rank)
end
-fun lines_of_mono_types ctxt mono type_enc =
+fun lines_of_mono_types ctxt generate_info mono type_enc =
(case type_enc of
Native _ => K []
- | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
- | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc))
+ | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
+ | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
let
@@ -2280,8 +2278,8 @@
fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
-fun line_of_guards_sym_decl ctxt mono type_enc n s j
- (s', T_args, T, _, ary, in_conj) =
+fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j
+ (s', T_args, T, _, ary, in_conj) =
let
val thy = Proof_Context.theory_of ctxt
val (role, maybe_negate) = honor_conj_sym_role in_conj
@@ -2310,11 +2308,11 @@
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
- NONE, isabelle_info inductiveN helper_rank)
+ NONE, isabelle_info generate_info inductiveN helper_rank)
end
-fun lines_of_tags_sym_decl ctxt mono type_enc n s
- (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s
+ (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val thy = Proof_Context.theory_of ctxt
val level = level_of_type_enc type_enc
@@ -2330,7 +2328,7 @@
val tag_with = tag_with_type ctxt mono type_enc NONE
fun formula c =
[Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
- isabelle_info non_rec_defN helper_rank)]
+ isabelle_info generate_info non_rec_defN helper_rank)]
in
if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
[]
@@ -2355,7 +2353,7 @@
end
| rationalize_decls _ decls = decls
-fun lines_of_sym_decls ctxt mono type_enc (s, decls) =
+fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
(case type_enc of
Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
| Guards (_, level) =>
@@ -2365,21 +2363,23 @@
val n = length decls
val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
in
- (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
+ (0 upto length decls - 1, decls)
+ |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)
end
| Tags (_, level) =>
if is_type_level_uniform level then
[]
else
let val n = length decls in
- (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
+ (0 upto n - 1 ~~ decls)
+ |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
end)
-fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
+fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab =
let
val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
- val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
- val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
+ val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts
+ val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms
in mono_lines @ decl_lines end
fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
@@ -2426,8 +2426,8 @@
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
-fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
- base_s0 types in_conj =
+fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0
+ types in_conj =
let
fun do_alias ary =
let
@@ -2464,31 +2464,32 @@
in
([tm1, tm2],
[Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
- isabelle_info non_rec_defN helper_rank)])
+ isabelle_info generate_info non_rec_defN helper_rank)])
|> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
else pair_append (do_alias (ary - 1)))
end
in do_alias end
-fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
+fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
(s, {min_ary, types, in_conj, ...} : sym_info) =
(case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
if String.isSubstring uncurried_alias_sep mangled_s then
let val base_s0 = mangled_s |> unmangled_invert_const in
- do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types
- in_conj min_ary
+ do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
+ base_s0 types in_conj min_ary
end
else
([], [])
| NONE => ([], []))
-fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
+fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
+ sym_tab0 sym_tab =
([], [])
|> uncurried_aliases
- ? Symtab.fold_rev
- (pair_append o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab)
- sym_tab
+ ? Symtab.fold_rev (pair_append
+ o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab)
+ sym_tab
val implicit_declsN = "Could-be-implicit typings"
val explicit_declsN = "Explicit typings"
@@ -2563,8 +2564,8 @@
val app_op_and_predicator_threshold = 45
-fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
- readable_names presimp hyp_ts concl_t facts =
+fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans
+ uncurried_aliases readable_names presimp hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val type_enc = type_enc |> adjust_type_enc format
@@ -2595,7 +2596,8 @@
val (ho_stuff, sym_tab) =
sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
- uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab
+ uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
+ sym_tab0 sym_tab
val (_, sym_tab) =
(ho_stuff, sym_tab)
|> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
@@ -2610,7 +2612,7 @@
val sym_decl_lines =
(conjs, helpers @ facts, uncurried_alias_eq_tms)
|> sym_decl_table_of_facts thy type_enc sym_tab
- |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
+ |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts
val datatype_decl_lines = map decl_line_of_datatype datatypes
val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
val num_facts = length facts
@@ -2618,13 +2620,14 @@
val pos = mode <> Exporter
val rank_of = rank_of_fact_num num_facts
val fact_lines =
- map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
+ map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
(0 upto num_facts - 1 ~~ facts)
- val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
- val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
+ val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
+ val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses
val helper_lines =
0 upto length helpers - 1 ~~ helpers
- |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
+ |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
+ (K default_rank))
val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
(* Reordering these might confuse the proof reconstruction code. *)
--- a/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 23:19:10 2015 +0100
@@ -227,7 +227,7 @@
*)
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
val (atp_problem, _, lifted, sym_tab) =
- generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
+ generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false []
@{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Dec 19 23:19:10 2015 +0100
@@ -575,11 +575,6 @@
fun dest_n_tuple 1 t = [t]
| dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
-type typedef_info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- prop_of_Rep: thm, set_name: string option, Abs_inverse: thm option,
- Rep_inverse: thm option}
-
fun typedef_info ctxt s =
if is_frac_type ctxt (Type (s, [])) then
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Dec 19 23:19:10 2015 +0100
@@ -235,6 +235,7 @@
val num_facts =
Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
|> Integer.min (length facts)
+ val generate_info = (case format of DFG _ => true | _ => false)
val strictness = if strict then Strict else Non_Strict
val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
val sound = is_type_enc_sound type_enc
@@ -273,8 +274,8 @@
generate_waldmeister_problem ctxt hyp_ts concl_t
#> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
else
- generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
- uncurried_aliases readable_names true hyp_ts concl_t
+ generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
+ lam_trans uncurried_aliases readable_names true hyp_ts concl_t
#> (fn (a, b, c, d) => (a, b, c, d, NONE)))
fun sel_weights () = atp_problem_selection_weights atp_problem
--- a/src/HOL/Tools/record.ML Sat Dec 19 23:16:47 2015 +0100
+++ b/src/HOL/Tools/record.ML Sat Dec 19 23:19:10 2015 +0100
@@ -1805,6 +1805,13 @@
distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
split_sels = [], split_sel_asms = [], case_eq_ifs = []};
+fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t
+ | lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t;
+
+fun add_spec_rule rule =
+ let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
+ Spec_Rules.add_global Spec_Rules.Equational ([head], [rule])
+ end;
(* definition *)
@@ -2040,7 +2047,7 @@
map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
||>> (Global_Theory.add_defs false o
map (rpair [Code.add_default_eqn_attribute]
- o apfst (Binding.concealed o Binding.name))) (*FIXME Spec_Rules (?)*)
+ o apfst (Binding.concealed o Binding.name)))
[make_spec, fields_spec, extend_spec, truncate_spec]);
val defs_ctxt = Proof_Context.init_global defs_thy;
@@ -2052,7 +2059,7 @@
(*selectors*)
val sel_conv_props =
- map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
+ map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
(*updates*)
fun mk_upd_prop i (c, T) =
@@ -2239,8 +2246,6 @@
sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
- val sels = map (fst o Logic.dest_equals o Thm.prop_of) sel_defs;
-
val final_thy =
thms_thy'
|> put_record name info
@@ -2253,6 +2258,7 @@
|> add_fieldext (extension_name, snd extension) names
|> add_code ext_tyco vs extT ext simps' ext_inject
|> add_ctr_sugar (Const ext) cases_scheme' ext_inject sel_convs'
+ |> fold add_spec_rule (sel_convs' @ upd_convs' @ derived_defs')
|> Sign.restore_naming thy0;
in final_thy end;