# HG changeset patch # User haftmann # Date 1284976536 -7200 # Node ID 9d75d65a1a7ab0f9e7e31a1941e517d833151813 # Parent 92a6ec7464e4425e963a95cda5010aa6c8928b10# Parent d154f988c247305a5fb8fcd3ef4306dc19aa10ae merged diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- 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 \ appending (x#xs) ys (x#zs)" + +lemma appending_alt_nil: "ys = zs \ appending [] ys zs" +by (auto intro: appending.intros) + +lemma appending_alt_cons: "xs' = x # xs \ appending xs ys zs \ zs' = x # zs \ 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 \ bool) [inductify, show_modes, show_intermediate_results, skip_proof] test . +code_pred (modes: o \ bool) [inductify] test . thm test.equation values "{rhs. test rhs}" diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Predicate_Compile_Examples/ROOT.ML --- 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"]) diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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; diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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 diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- 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 diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 diff -r d154f988c247 -r 9d75d65a1a7a src/HOL/Tools/try.ML --- 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"