--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 11:55:21 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Sep 20 11:55:36 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/Sledgehammer/metis_reconstruct.ML Mon Sep 20 11:55:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 11:55:36 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:55:21 2010 +0200
+++ b/src/HOL/Tools/try.ML Mon Sep 20 11:55:36 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"