--- a/doc-src/Classes/style.sty Mon Sep 20 11:38:14 2010 +0200
+++ b/doc-src/Classes/style.sty Mon Sep 20 12:03:11 2010 +0200
@@ -17,9 +17,6 @@
%% typographic conventions
\newcommand{\qt}[1]{``{#1}''}
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
%% quote environment
\isakeeptag{quote}
\renewenvironment{quote}
--- a/doc-src/Codegen/style.sty Mon Sep 20 11:38:14 2010 +0200
+++ b/doc-src/Codegen/style.sty Mon Sep 20 12:03:11 2010 +0200
@@ -17,9 +17,6 @@
\newcommand{\qt}[1]{``{#1}''}
\newcommand{\ditem}[1]{\item[\isastyletext #1]}
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
%% quote environment
\isakeeptag{quote}
\renewenvironment{quote}
--- a/doc-src/isabelle.sty Mon Sep 20 11:38:14 2010 +0200
+++ b/doc-src/isabelle.sty Mon Sep 20 12:03:11 2010 +0200
@@ -1,5 +1,3 @@
-%%
-%%
%%
%% macros for Isabelle generated LaTeX output
%%
@@ -48,6 +46,8 @@
{\begin{trivlist}\begin{isabellebody}\item\relax}
{\end{isabellebody}\end{trivlist}}
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+
\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
\newcommand{\isaindent}[1]{\hphantom{#1}}
--- a/doc-src/more_antiquote.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/doc-src/more_antiquote.ML Mon Sep 20 12:03:11 2010 +0200
@@ -29,7 +29,7 @@
let
val thy = ProofContext.theory_of ctxt;
val const = Code.check_const thy raw_const;
- val (_, eqngr) = Code_Preproc.obtain thy [const] [];
+ val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
val thms = Code_Preproc.cert eqngr const
|> Code.equations_of_cert thy
--- a/lib/texinputs/isabelle.sty Mon Sep 20 11:38:14 2010 +0200
+++ b/lib/texinputs/isabelle.sty Mon Sep 20 12:03:11 2010 +0200
@@ -46,6 +46,8 @@
{\begin{trivlist}\begin{isabellebody}\item\relax}
{\end{isabellebody}\end{trivlist}}
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+
\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
\newcommand{\isaindent}[1]{\hphantom{#1}}
--- a/src/HOL/Library/Multiset.thy Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 20 12:03:11 2010 +0200
@@ -779,8 +779,8 @@
by (induct xs) (auto simp: add_ac)
lemma count_filter:
- "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
-by (induct xs) auto
+ "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
+ by (induct xs) auto
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
apply (induct ls arbitrary: i)
@@ -809,12 +809,40 @@
by (auto simp add: length_remove1 dest: length_pos_if_in_set)
qed
-lemma (in linorder) multiset_of_insort [simp]:
- "multiset_of (insort x xs) = {#x#} + multiset_of xs"
+lemma multiset_of_eq_length_filter:
+ assumes "multiset_of xs = multiset_of ys"
+ shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
+proof (cases "z \<in># multiset_of xs")
+ case False
+ moreover have "\<not> z \<in># multiset_of ys" using assms False by simp
+ ultimately show ?thesis by (simp add: count_filter)
+next
+ case True
+ moreover have "z \<in># multiset_of ys" using assms True by simp
+ show ?thesis using assms proof (induct xs arbitrary: ys)
+ case Nil then show ?case by simp
+ next
+ case (Cons x xs)
+ from `multiset_of (x # xs) = multiset_of ys` [symmetric]
+ have *: "multiset_of xs = multiset_of (remove1 x ys)"
+ and "x \<in> set ys"
+ by (auto simp add: mem_set_multiset_eq)
+ from * have "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) (remove1 x ys))" by (rule Cons.hyps)
+ moreover from `x \<in> set ys` have "length (filter (\<lambda>y. x = y) ys) > 0" by (simp add: filter_empty_conv)
+ ultimately show ?case using `x \<in> set ys`
+ by (simp add: filter_remove1) (auto simp add: length_remove1)
+ qed
+qed
+
+context linorder
+begin
+
+lemma multiset_of_insort_key [simp]:
+ "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
by (induct xs) (simp_all add: ac_simps)
-
-lemma (in linorder) multiset_of_sort [simp]:
- "multiset_of (sort xs) = multiset_of xs"
+
+lemma multiset_of_sort_key [simp]:
+ "multiset_of (sort_key k xs) = multiset_of xs"
by (induct xs) (simp_all add: ac_simps)
text {*
@@ -822,18 +850,42 @@
@{text "f"} with @{text "f xs = ys"} behaves like sort.
*}
-lemma (in linorder) properties_for_sort:
- "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
-proof (induct xs arbitrary: ys)
+lemma properties_for_sort_key:
+ assumes "multiset_of ys = multiset_of xs"
+ and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs"
+ and "sorted (map f ys)"
+ shows "sort_key f xs = ys"
+using assms proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
- then have "x \<in> set ys"
- by (auto simp add: mem_set_multiset_eq intro!: ccontr)
- with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
- by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
+ from Cons.prems(2) have
+ "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs"
+ by (simp add: filter_remove1)
+ with Cons.prems have "sort_key f xs = remove1 x ys"
+ by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
+ moreover from Cons.prems have "x \<in> set ys"
+ by (auto simp add: mem_set_multiset_eq intro!: ccontr)
+ ultimately show ?case using Cons.prems by (simp add: insort_key_remove1)
qed
+lemma properties_for_sort:
+ assumes multiset: "multiset_of ys = multiset_of xs"
+ and "sorted ys"
+ shows "sort xs = ys"
+proof (rule properties_for_sort_key)
+ from multiset show "multiset_of ys = multiset_of xs" .
+ from `sorted ys` show "sorted (map (\<lambda>x. x) ys)" by simp
+ from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
+ by (rule multiset_of_eq_length_filter)
+ then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
+ by simp
+ then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
+ by (simp add: replicate_length_filter)
+qed
+
+end
+
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
by (induct xs) (auto intro: order_trans)
--- a/src/HOL/List.thy Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/List.thy Mon Sep 20 12:03:11 2010 +0200
@@ -3264,6 +3264,10 @@
apply auto
done
+lemma replicate_length_filter:
+ "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
+ by (induct xs) auto
+
subsubsection{*@{text rotate1} and @{text rotate}*}
@@ -3738,24 +3742,43 @@
lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
by (cases xs) auto
+lemma sorted_map_remove1:
+ "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
+ by (induct xs) (auto simp add: sorted_Cons)
+
lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
-by(induct xs)(auto simp add: sorted_Cons)
-
-lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
- \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
-proof (induct xs)
+ using sorted_map_remove1 [of "\<lambda>x. x"] by simp
+
+lemma insort_key_remove1:
+ assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
+ shows "insort_key f a (remove1 a xs) = xs"
+using assms proof (induct xs)
case (Cons x xs)
- thus ?case
+ then show ?case
proof (cases "x = a")
case False
- hence "f x \<noteq> f a" using Cons.prems by auto
- hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
- thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+ then have "f x \<noteq> f a" using Cons.prems by auto
+ then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+ with `f x \<noteq> f a` show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
qed (auto simp: sorted_Cons insort_is_Cons)
qed simp
-lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
-using insort_key_remove1[where f="\<lambda>x. x"] by simp
+lemma insort_remove1:
+ assumes "a \<in> set xs" and "sorted xs"
+ shows "insort a (remove1 a xs) = xs"
+proof (rule insort_key_remove1)
+ from `a \<in> set xs` show "a \<in> set xs" .
+ from `sorted xs` show "sorted (map (\<lambda>x. x) xs)" by simp
+ from `a \<in> set xs` have "a \<in> set (filter (op = a) xs)" by auto
+ then have "set (filter (op = a) xs) \<noteq> {}" by auto
+ then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
+ then have "length (filter (op = a) xs) > 0" by simp
+ then obtain n where n: "Suc n = length (filter (op = a) xs)"
+ by (cases "length (filter (op = a) xs)") simp_all
+ moreover have "replicate (Suc n) a = a # replicate n a"
+ by simp
+ ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
+qed
lemma sorted_remdups[simp]:
"sorted l \<Longrightarrow> sorted (remdups l)"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 12:03:11 2010 +0200
@@ -216,6 +216,37 @@
qed
qed
+subsection {* Named alternative rules *}
+
+inductive appending
+where
+ nil: "appending [] ys ys"
+| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
+
+lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
+by (auto intro: appending.intros)
+
+lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
+by (auto intro: appending.intros)
+
+text {* With code_pred_intro, we can give fact names to the alternative rules,
+ which are used for the code_pred command. *}
+
+declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
+
+code_pred appending
+proof -
+ case appending
+ from prems show thesis
+ proof(cases)
+ case nil
+ from alt_nil nil show thesis by auto
+ next
+ case cons
+ from alt_cons cons show thesis by fastsimp
+ qed
+qed
+
subsection {* Preprocessor Inlining *}
definition "equals == (op =)"
@@ -1612,13 +1643,13 @@
rule ''A'' [TS ''b'']}, ''S'')"
-code_pred [inductify,skip_proof] derives .
+code_pred [inductify, skip_proof] derives .
thm derives.equation
definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
-code_pred (modes: o \<Rightarrow> bool) [inductify, show_modes, show_intermediate_results, skip_proof] test .
+code_pred (modes: o \<Rightarrow> bool) [inductify] test .
thm test.equation
values "{rhs. test rhs}"
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Mon Sep 20 12:03:11 2010 +0200
@@ -1,2 +1,5 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
-if getenv "PROLOG_HOME" = "" then () else (use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"]; setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"])
+if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
+ (warning "No prolog system found - could not use example theories that require a prolog system"; ())
+else
+ (use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"]; setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"])
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 20 12:03:11 2010 +0200
@@ -662,6 +662,18 @@
val rename_vars_program = map rename_vars_clause
+(* post processing of generated prolog program *)
+
+fun post_process ctxt options (p, constant_table) =
+ (p, constant_table)
+ |> (if #ensure_groundness options then
+ add_ground_predicates ctxt (#limited_types options)
+ else I)
+ |> add_limited_predicates (#limited_predicates options)
+ |> apfst (fold replace (#replacing options))
+ |> apfst (reorder_manually (#manual_reorder options))
+ |> apfst rename_vars_program
+
(* code printer *)
fun write_arith_op Plus = "+"
@@ -704,9 +716,9 @@
"eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
rel ^ "(" ^ space_implode ", " (map write_term args) ^ "), Sols), writelist(Sols).\n" ^
"writelist([]).\n" ^
- "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^
+ "writelist([(" ^ space_implode ", " vnames ^ ")|SolutionTail]) :- " ^
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
- "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
+ "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n"
val swi_prolog_prelude =
"#!/usr/bin/swipl -q -t main -f\n\n" ^
@@ -809,12 +821,10 @@
fun run (timeout, system) p (query_rel, args) vnames nsols =
let
- val p' = rename_vars_program p
- val _ = tracing "Renaming variable names..."
val renaming = fold mk_renaming (fold add_vars args vnames) []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
val args' = map (rename_vars_term renaming) args
- val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p'
+ val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
val _ = tracing ("Generated prolog program:\n" ^ prog)
val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
(File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
@@ -902,12 +912,7 @@
val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
- |> (if #ensure_groundness options then
- add_ground_predicates ctxt' (#limited_types options)
- else I)
- |> add_limited_predicates (#limited_predicates options)
- |> apfst (fold replace (#replacing options))
- |> apfst (reorder_manually (#manual_reorder options))
+ |> post_process ctxt' options
val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
val args' = map (translate_term ctxt constant_table') all_args
val _ = tracing "Running prolog program..."
@@ -970,44 +975,20 @@
(* quickcheck generator *)
-(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
-
-fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
- | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
- | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
fun quickcheck ctxt t size =
let
val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
- val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt [] vs
- val Ts = map snd vs'
- val t'' = subst_bounds (map Free (rev vs'), t')
- val (prems, concl) = strip_horn t''
- val constname = "quickcheck"
- val full_constname = Sign.full_bname thy constname
- val constT = Ts ---> @{typ bool}
- val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
- val const = Const (full_constname, constT)
- val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
- HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn _ => Skip_Proof.cheat_tac thy1
- val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+ val ((((full_constname, constT), vs'), intro), thy1) =
+ Predicate_Compile_Aux.define_quickcheck_predicate t thy
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
- val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
+ val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, true) ctxt' full_constname
- |> add_ground_predicates ctxt' (#limited_types options)
- |> add_limited_predicates (#limited_predicates options)
- |> apfst (fold replace (#replacing options))
- |> apfst (reorder_manually (#manual_reorder options))
+ |> post_process ctxt' (set_ensure_groundness options)
val _ = tracing "Running prolog program..."
val system_config = System_Config.get (Context.Proof ctxt)
val tss = run (#timeout system_config, #prolog_system system_config)
@@ -1015,7 +996,7 @@
val _ = tracing "Restoring terms..."
val res =
case tss of
- [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+ [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
| _ => NONE
val empty_report = ([], false)
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 20 12:03:11 2010 +0200
@@ -148,6 +148,8 @@
val remove_equalities : theory -> thm -> thm
val remove_pointless_clauses : thm -> thm list
val peephole_optimisation : theory -> thm -> thm option
+ val define_quickcheck_predicate :
+ term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
end;
structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
@@ -909,4 +911,34 @@
(process_False (process_True (prop_of (process intro))))
end
+(* defining a quickcheck predicate *)
+
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
+ | strip_imp_prems _ = [];
+
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
+ | strip_imp_concl A = A : term;
+
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+
+fun define_quickcheck_predicate t thy =
+ let
+ val (vs, t') = strip_abs t
+ val vs' = Variable.variant_frees (ProofContext.init_global thy) [] vs
+ val t'' = subst_bounds (map Free (rev vs'), t')
+ val (prems, concl) = strip_horn t''
+ val constname = "quickcheck"
+ val full_constname = Sign.full_bname thy constname
+ val constT = map snd vs' ---> @{typ bool}
+ val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+ val const = Const (full_constname, constT)
+ val t = Logic.list_implies
+ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+ HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
+ val tac = fn _ => Skip_Proof.cheat_tac thy1
+ val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+ in
+ ((((full_constname, constT), vs'), intro), thy1)
+ end
+
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 12:03:11 2010 +0200
@@ -28,7 +28,7 @@
val all_random_modes_of : Proof.context -> (string * mode list) list
val intros_of : Proof.context -> string -> thm list
val intros_graph_of : Proof.context -> thm list Graph.T
- val add_intro : thm -> theory -> theory
+ val add_intro : string option * thm -> theory -> theory
val set_elim : thm -> theory -> theory
val register_alternative_function : string -> mode -> string -> theory -> theory
val alternative_compilation_of_global : theory -> string -> mode ->
@@ -216,7 +216,7 @@
PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
datatype pred_data = PredData of {
- intros : thm list,
+ intros : (string option * thm) list,
elim : thm option,
function_names : (compilation * (mode * string) list) list,
predfun_data : (mode * predfun_data) list,
@@ -237,7 +237,7 @@
| eq_option eq _ = false
fun eq_pred_data (PredData d1, PredData d2) =
- eq_list Thm.eq_thm (#intros d1, #intros d2) andalso
+ eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
eq_option Thm.eq_thm (#elim d1, #elim d2)
structure PredData = Theory_Data
@@ -261,7 +261,9 @@
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
-val intros_of = #intros oo the_pred_data
+val intros_of = map snd o #intros oo the_pred_data
+
+val names_of = map fst o #intros oo the_pred_data
fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
of NONE => error ("No elimination rule for predicate " ^ quote name)
@@ -316,7 +318,7 @@
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
val intros_graph_of =
- Graph.map (K (#intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
+ Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
(* diagnostic display functions *)
@@ -654,7 +656,7 @@
val elim =
prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
in
- mk_pred_data ((intros, SOME elim), no_compilation)
+ mk_pred_data ((map (pair NONE) intros, SOME elim), no_compilation)
end
| NONE => error ("No such predicate: " ^ quote name)
@@ -668,21 +670,21 @@
fun depending_preds_of ctxt (key, value) =
let
- val intros = (#intros o rep_pred_data) value
+ val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
in
- fold Term.add_const_names (map Thm.prop_of intros) []
+ fold Term.add_const_names intros []
|> filter (fn c => (not (c = key)) andalso
(is_inductive_predicate ctxt c orelse is_registered ctxt c))
end;
-fun add_intro thm thy =
+fun add_intro (opt_case_name, thm) thy =
let
val (name, T) = dest_Const (fst (strip_intro_concl thm))
fun cons_intro gr =
case try (Graph.get_node gr) name of
SOME pred_data => Graph.map_node name (map_pred_data
- (apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr
- | NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr
+ (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))) gr
+ | NONE => Graph.new_node (name, mk_pred_data (([(opt_case_name, thm)], NONE), no_compilation)) gr
in PredData.map cons_intro thy end
fun set_elim thm =
@@ -694,7 +696,7 @@
fun register_predicate (constname, pre_intros, pre_elim) thy =
let
- val intros = map (preprocess_intro thy) pre_intros
+ val intros = map (pair NONE o preprocess_intro thy) pre_intros
val elim = preprocess_elim (ProofContext.init_global thy) pre_elim
in
if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
@@ -3042,9 +3044,10 @@
(* code_pred_intro attribute *)
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+fun attrib' f opt_case_name =
+ Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I);
-val code_pred_intro_attrib = attrib add_intro;
+val code_pred_intro_attrib = attrib' add_intro NONE;
(*FIXME
@@ -3052,7 +3055,7 @@
*)
val setup = PredData.put (Graph.empty) #>
- Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro))
+ Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
"adding alternative introduction rules for code generation of inductive predicates"
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
@@ -3075,12 +3078,14 @@
in mk_casesrule lthy' pred intros end
val cases_rules = map mk_cases preds
val cases =
- map (fn case_rule => Rule_Cases.Case {fixes = [],
- assumes = [("", Logic.strip_imp_prems case_rule)],
- binds = [], cases = []}) cases_rules
+ map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
+ assumes = ("", Logic.strip_imp_prems case_rule)
+ :: (map_filter (fn (fact_name, fact) => Option.map (rpair [fact]) fact_name)
+ ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
+ binds = [], cases = []}) preds cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
- |> fold Variable.auto_fixes cases_rules
+ |> fold Variable.auto_fixes cases_rules
|> ProofContext.add_cases true case_env
fun after_qed thms goal_ctxt =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Sep 20 12:03:11 2010 +0200
@@ -187,14 +187,6 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
- | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
- | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
-
fun cpu_time description f =
let
val start = start_timing ()
@@ -205,23 +197,11 @@
fun compile_term compilation options ctxt t =
let
val thy = Theory.copy (ProofContext.theory_of ctxt)
- val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt [] vs
- val t'' = subst_bounds (map Free (rev vs'), t')
- val (prems, concl) = strip_horn t''
- val constname = "pred_compile_quickcheck"
- val full_constname = Sign.full_bname thy constname
- val constT = map snd vs' ---> @{typ bool}
- val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
- val const = Const (full_constname, constT)
- val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
- HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn _ => Skip_Proof.cheat_tac thy1
- val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+ val ((((full_constname, constT), vs'), intro), thy1) =
+ Predicate_Compile_Aux.define_quickcheck_predicate t thy
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val (thy3, preproc_time) = cpu_time "predicate preprocessing"
- (fn () => Predicate_Compile.preprocess options const thy2)
+ (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
(fn () =>
case compilation of
--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Sep 20 12:03:11 2010 +0200
@@ -304,18 +304,19 @@
let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
in (Const (n, Us ---> T), sels) end
-fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
- (case Datatype.get_info (ProofContext.theory_of ctxt) n of
- NONE => NONE (* FIXME: also use Record.get_info *)
- | SOME {descr, ...} =>
- let
- val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
- (sort (int_ord o pairself fst) descr)
- val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
- in
- SOME (descr |> map (fn (i, (_, _, cs)) =>
- (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
- end)
+fun lookup_datatype ctxt n Ts =
+ if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE
+ else
+ Datatype.get_info (ProofContext.theory_of ctxt) n
+ |> Option.map (fn {descr, ...} =>
+ let
+ val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
+ (sort (int_ord o pairself fst) descr)
+ val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
+ in
+ descr |> map (fn (i, (_, _, cs)) =>
+ (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
+ end)
fun relaxed thms = (([], thms), map prop_of thms)
--- a/src/HOL/Tools/SMT/z3_model.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML Mon Sep 20 12:03:11 2010 +0200
@@ -6,7 +6,8 @@
signature Z3_MODEL =
sig
- val parse_counterex: SMT_Translate.recon -> string list -> term list
+ val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
+ term list
end
structure Z3_Model: Z3_MODEL =
@@ -15,82 +16,156 @@
(* counterexample expressions *)
datatype expr = True | False | Number of int * int option | Value of int |
- Array of array
+ Array of array | App of string * expr list
and array = Fresh of expr | Store of (array * expr) * expr
(* parsing *)
val space = Scan.many Symbol.is_ascii_blank
-fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"
-fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- Scan.$$ "}")
+fun spaced p = p --| space
+fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
+fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}")
val digit = (fn
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE)
-val nat_num = Scan.repeat1 (Scan.some digit) >>
- (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
-val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
- (fn sign => nat_num >> sign)
+val nat_num = spaced (Scan.repeat1 (Scan.some digit) >>
+ (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
+val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+ (fn sign => nat_num >> sign))
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
-val name = Scan.many1 is_char >> implode
+val name = spaced (Scan.many1 is_char >> implode)
+
+fun $$$ s = spaced (Scan.this_string s)
-fun array_expr st = st |>
- in_parens (space |-- (
- Scan.this_string "const" |-- expr >> Fresh ||
- Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))
+fun array_expr st = st |> in_parens (
+ $$$ "const" |-- expr >> Fresh ||
+ $$$ "store" |-- array_expr -- expr -- expr >> Store)
-and expr st = st |> (space |-- (
- Scan.this_string "true" >> K True ||
- Scan.this_string "false" >> K False ||
- int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||
- Scan.this_string "val!" |-- nat_num >> Value ||
- array_expr >> Array))
+and expr st = st |> (
+ $$$ "true" >> K True ||
+ $$$ "false" >> K False ||
+ int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
+ $$$ "val!" |-- nat_num >> Value ||
+ name >> (App o rpair []) ||
+ array_expr >> Array ||
+ in_parens (name -- Scan.repeat1 expr) >> App)
-val mapping = space -- Scan.this_string "->"
-val value = mapping |-- expr
-
-val args_case = Scan.repeat expr -- value
-val else_case = space -- Scan.this_string "else" |-- value >>
- pair ([] : expr list)
+fun args st = ($$$ "->" >> K [] || expr ::: args) st
+val args_case = args -- expr
+val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list)
val func =
let fun cases st = (else_case >> single || args_case ::: cases) st
in in_braces cases end
-val cex = space |-- Scan.repeat (space |-- name --| mapping --
- (func || expr >> (single o pair [])))
+val cex = space |--
+ Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
fun read_cex ls =
- explode (cat_lines ls)
+ maps (cons "\n" o explode) ls
|> try (fst o Scan.finite Symbol.stopper cex)
|> the_default []
+(* normalization *)
+
+local
+ fun matches terms f n =
+ (case Symtab.lookup terms n of
+ NONE => false
+ | SOME t => f t)
+
+ fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
+in
+
+fun reduce_function (n, [c]) = SOME ((n, 0), [c])
+ | reduce_function (n, cases) =
+ let val (patterns, else_case as (_, e)) = split_last cases
+ in
+ (case patterns of
+ [] => NONE
+ | (args, _) :: _ => SOME ((n, length args),
+ filter_out (equal e o snd) patterns @ [else_case]))
+ end
+
+fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
+
+fun substitute_constants terms =
+ let
+ fun check vs1 [] = rev vs1
+ | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
+ if matches terms (fn Free _ => true | _ => false) n orelse k > 0
+ then check (v :: vs1) vs2
+ else
+ let
+ fun sub (e as Value j) = if i = j then App (n, []) else e
+ | sub e = e
+ in check (map (subst sub) vs1) (map (subst sub) vs2) end
+ | check vs1 (v :: vs2) = check (v :: vs1) vs2
+ in check [] end
+
+fun remove_int_nat_coercions terms vs =
+ let
+ fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
+
+ val ints =
+ find_first (match [@{term int}]) vs
+ |> Option.map (fn (_, cases) =>
+ let val (cs, (_, e)) = split_last cases
+ in (e, map (apfst hd) cs) end)
+ fun nat_of (v as Value _) =
+ (case ints of
+ NONE => v
+ | SOME (e, tab) => the_default e (AList.lookup (op =) tab v))
+ | nat_of e = e
+ in
+ map (subst nat_of) vs
+ |> filter_out (match [@{term int}, @{term nat}])
+ end
+
+fun filter_valid_valuations terms = map_filter (fn
+ (_, []) => NONE
+ | ((n, i), cases) =>
+ let
+ fun valid_expr (Array a) = valid_array a
+ | valid_expr (App (n, es)) =
+ Symtab.defined terms n andalso forall valid_expr es
+ | valid_expr _ = true
+ and valid_array (Fresh e) = valid_expr e
+ | valid_array (Store ((a, e1), e2)) =
+ valid_array a andalso valid_expr e1 andalso valid_expr e2
+ fun valid_case (es, e) = forall valid_expr (e :: es)
+ in
+ if not (forall valid_case cases) then NONE
+ else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
+ end)
+
+end
+
+
(* translation into terms *)
-fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)
+fun with_context ctxt terms f vs =
+ fst (fold_map f vs (ctxt, terms, Inttab.empty))
-fun with_name_context tab f xs =
- let
- val ns = Symtab.fold (Term.add_free_names o snd) tab []
- val nctxt = Name.make_context ns
- in fst (fold_map f xs (Inttab.empty, nctxt)) end
+fun fresh_term T (ctxt, terms, values) =
+ let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
+ in (Free (n, T), (ctxt', terms, values)) end
-fun fresh_term T (tab, nctxt) =
- let val (n, nctxt') = yield_singleton Name.variants "" nctxt
- in (Free (n, T), (tab, nctxt')) end
-
-fun term_of_value T i (cx as (tab, _)) =
- (case Inttab.lookup tab i of
+fun term_of_value T i (cx as (_, _, values)) =
+ (case Inttab.lookup values i of
SOME t => (t, cx)
| NONE =>
- let val (t, (tab', nctxt')) = fresh_term T cx
- in (t, (Inttab.update (i, t) tab', nctxt')) end)
+ let val (t, (ctxt', terms', values')) = fresh_term T cx
+ in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
+
+fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
fun trans_expr _ True = pair @{term True}
| trans_expr _ False = pair @{term False}
@@ -100,6 +175,13 @@
HOLogic.mk_number T i $ HOLogic.mk_number T j)
| trans_expr T (Value i) = term_of_value T i
| trans_expr T (Array a) = trans_array T a
+ | trans_expr _ (App (n, es)) =
+ let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
+ in
+ get_term n #-> (fn t =>
+ fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
+ Term.list_comb o pair t)
+ end
and trans_array T a =
let val dT = Term.domain_type T and rT = Term.range_type T
@@ -112,35 +194,60 @@
Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
end
-fun trans_pat i T f x =
- f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>
- (fn (u, (us, t)) => (u :: us, t))
+fun trans_pattern T ([], e) = trans_expr T e #>> pair []
+ | trans_pattern T (arg :: args, e) =
+ trans_expr (Term.domain_type T) arg ##>>
+ trans_pattern (Term.range_type T) (args, e) #>>
+ (fn (arg', (args', e')) => (arg' :: args', e'))
-and trans i T ([], v) =
- if i > 0 then trans_pat i T fresh_term ([], v)
- else trans_expr T v #>> pair []
- | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
+fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
+
+fun split_type T = (Term.domain_type T, Term.range_type T)
-fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
-fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
- | mk_eq t (us, u) = mk_eq' t us u
+fun mk_update ([], u) _ = u
+ | mk_update ([t], u) f =
+ uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+ | mk_update (t :: ts, u) f =
+ let
+ val (dT, rT) = split_type (Term.fastype_of f)
+ val (dT', rT') = split_type rT
+ in
+ mk_fun_upd dT rT $ f $ t $
+ mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
+ end
+
+fun mk_lambda Ts (t, pats) =
+ fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
-fun translate (t, cs) =
- let val T = Term.fastype_of t
- in
- (case (can HOLogic.dest_number t, cs) of
- (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
- | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
- | _ => raise TERM ("translate: no cases", [t]))
- end
+fun translate' T i [([], e)] =
+ if i = 0 then trans_expr T e
+ else
+ let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
+ in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
+ | translate' T i cases =
+ let
+ val (pat_cases, def) = split_last cases |> apsnd snd
+ val ((Us1, Us2), U) = Term.strip_type T |>> chop i
+ in
+ trans_expr (Us2 ---> U) def ##>>
+ fold_map (trans_pattern T) pat_cases #>>
+ mk_lambda Us1
+ end
+
+fun translate ((t, i), cases) =
+ translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
(* overall procedure *)
-fun parse_counterex ({terms, ...} : SMT_Translate.recon) ls =
+fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
read_cex ls
- |> map_filter (lookup_term terms)
- |> with_name_context terms translate
- |> flat
+ |> map_filter reduce_function
+ |> drop_skolem_constants terms
+ |> substitute_constants terms
+ |> remove_int_nat_coercions terms
+ |> filter_valid_valuations terms
+ |> with_context ctxt terms translate
end
+
--- a/src/HOL/Tools/SMT/z3_solver.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_solver.ML Mon Sep 20 12:03:11 2010 +0200
@@ -41,11 +41,11 @@
get_options ctxt
|> add ["-smt"]
-fun raise_cex real recon ls =
- let val cex = Z3_Model.parse_counterex recon ls
+fun raise_cex ctxt real recon ls =
+ let val cex = Z3_Model.parse_counterex ctxt recon ls
in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
-fun if_unsat f (output, recon) =
+fun if_unsat f (output, recon) ctxt =
let
fun jnk l =
String.isPrefix "WARNING" l orelse
@@ -53,13 +53,13 @@
forall Symbol.is_ascii_blank (Symbol.explode l)
val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
in
- if String.isPrefix "unsat" l then f (ls, recon)
- else if String.isPrefix "sat" l then raise_cex true recon ls
- else if String.isPrefix "unknown" l then raise_cex false recon ls
+ if String.isPrefix "unsat" l then f (ls, recon) ctxt
+ else if String.isPrefix "sat" l then raise_cex ctxt true recon ls
+ else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls
else raise SMT_Solver.SMT (solver_name ^ " failed")
end
-val core_oracle = if_unsat (K @{cprop False})
+val core_oracle = uncurry (if_unsat (K (K @{cprop False})))
val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
@@ -72,7 +72,7 @@
{command = {env_var=env_var, remote_name=SOME solver_name},
arguments = cmdline_options ctxt,
interface = Z3_Interface.interface with_datatypes,
- reconstruct = if with_proof then prover else pair o oracle}
+ reconstruct = if with_proof then prover else (fn r => `(oracle o pair r))}
end
val setup =
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Sep 20 12:03:11 2010 +0200
@@ -11,7 +11,7 @@
sig
type mode = Metis_Translate.mode
- val trace: bool Unsynchronized.ref
+ val trace : bool Unsynchronized.ref
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val replay_one_inference :
Proof.context -> mode -> (string * term) list
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 12:03:11 2010 +0200
@@ -23,7 +23,6 @@
open Metis_Translate
open Metis_Reconstruct
-val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
@@ -139,6 +138,8 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+val preproc_ss = HOL_basic_ss addsimps @{thms all_simps [symmetric]}
+
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
@@ -147,9 +148,14 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt i st0
+ Tactical.SOLVED'
+ ((TRY o Simplifier.simp_tac preproc_ss)
+ THEN'
+ (REPEAT_DETERM o match_tac @{thms allI})
+ THEN'
+ TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+ ctxt) i st0
end
val metis_tac = generic_metis_tac HO
--- a/src/HOL/Tools/try.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/HOL/Tools/try.ML Mon Sep 20 12:03:11 2010 +0200
@@ -58,18 +58,19 @@
Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
end
-fun do_named_method_on_first_goal name timeout_opt st =
+fun do_named_method (name, all_goals) timeout_opt st =
do_generic timeout_opt
- (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
- else "")) I (#goal o Proof.goal)
+ (name ^ (if all_goals andalso
+ nprems_of (#goal (Proof.goal st)) > 1 then
+ "[1]"
+ else
+ "")) I (#goal o Proof.goal)
(apply_named_method_on_first_goal name (Proof.context_of st)) st
-val all_goals_named_methods = ["auto"]
-val first_goal_named_methods =
- ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
-val do_methods =
- map do_named_method_on_first_goal all_goals_named_methods @
- map do_named_method first_goal_named_methods
+val named_methods =
+ [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
+ ("force", false), ("blast", false), ("arith", false)]
+val do_methods = map do_named_method named_methods
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
--- a/src/Pure/Isar/code.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/Pure/Isar/code.ML Mon Sep 20 12:03:11 2010 +0200
@@ -543,7 +543,8 @@
handle TERM _ => bad "Not an abstract equation";
val (rep_const, ty) = dest_Const rep;
val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
- handle TERM _ => bad "Not an abstract equation";
+ handle TERM _ => bad "Not an abstract equation"
+ | TYPE _ => bad "Not an abstract equation";
val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
| NONE => ();
--- a/src/Tools/Code/code_printer.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Mon Sep 20 12:03:11 2010 +0200
@@ -147,13 +147,13 @@
else s1 ^ s ^ s2
end;
-fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs)
+fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs
| plain_text (XML.Text s) = s
fun format presentation_names width =
Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
#> YXML.parse_body
- #> (if null presentation_names then implode o map plain_text
+ #> (if null presentation_names then maps_string "" plain_text
else maps_string "\n\n" (filter_presentation presentation_names false))
#> suffix "\n";
--- a/src/Tools/Code/code_runtime.ML Mon Sep 20 11:38:14 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon Sep 20 12:03:11 2010 +0200
@@ -63,7 +63,7 @@
fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
(the_default target some_target) NONE "Code" [];
-fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args =
+fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
let
val ctxt = ProofContext.init_global thy;
val _ = if Code_Thingol.contains_dictvar t then