# HG changeset patch # User bulwahn # Date 1258624183 -3600 # Node ID bc75dbbbf3e6c5dbc4d70502bbac69469daa0798 # Parent 47b7c9e0bf6e62b89b6e3b282d36924195905a27# Parent 7ead0ccf6cbd35437ea43032a613601be2ee431f merged diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/HOL.thy Thu Nov 19 10:49:43 2009 +0100 @@ -2060,7 +2060,6 @@ setup {* Predicate_Compile_Alternative_Defs.setup #> Predicate_Compile_Inline_Defs.setup - #> Predicate_Compile_Preproc_Const_Defs.setup *} diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Predicate.thy Thu Nov 19 10:49:43 2009 +0100 @@ -570,6 +570,9 @@ definition if_pred :: "bool \ unit pred" where if_pred_eq: "if_pred b = (if b then single () else \)" +definition holds :: "unit pred \ bool" where + holds_eq: "holds P = eval P ()" + definition not_pred :: "unit pred \ unit pred" where not_pred_eq: "not_pred P = (if eval P () then \ else single ())" @@ -592,7 +595,54 @@ lemma not_predE': "eval (not_pred P) x \ (\ eval P x \ thesis) \ thesis" unfolding not_pred_eq by (auto split: split_if_asm elim: botE) +lemma "f () = False \ f () = True" +by simp +lemma closure_of_bool_cases: +assumes "(f :: unit \ bool) = (%u. False) \ P f" +assumes "f = (%u. True) \ P f" +shows "P f" +proof - + have "f = (%u. False) \ f = (%u. True)" + apply (cases "f ()") + apply (rule disjI2) + apply (rule ext) + apply (simp add: unit_eq) + apply (rule disjI1) + apply (rule ext) + apply (simp add: unit_eq) + done + from this prems show ?thesis by blast +qed + +lemma unit_pred_cases: +assumes "P \" +assumes "P (single ())" +shows "P Q" +using assms +unfolding bot_pred_def Collect_def empty_def single_def +apply (cases Q) +apply simp +apply (rule_tac f="fun" in closure_of_bool_cases) +apply auto +apply (subgoal_tac "(%x. () = x) = (%x. True)") +apply auto +done + +lemma holds_if_pred: + "holds (if_pred b) = b" +unfolding if_pred_eq holds_eq +by (cases b) (auto intro: singleI elim: botE) + +lemma if_pred_holds: + "if_pred (holds P) = P" +unfolding if_pred_eq holds_eq +by (rule unit_pred_cases) (auto intro: singleI elim: botE) + +lemma is_empty_holds: + "is_empty P \ \ holds P" +unfolding is_empty_def holds_eq +by (rule unit_pred_cases) (auto elim: botE intro: singleI) subsubsection {* Implementation *} @@ -838,7 +888,7 @@ bind (infixl "\=" 70) hide (open) type pred seq -hide (open) const Pred eval single bind is_empty singleton if_pred not_pred +hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the end diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 19 10:49:43 2009 +0100 @@ -111,10 +111,10 @@ in Options { expected_modes = Option.map (pair const) expected_modes, - proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [], + proposed_modes = Option.map (pair const o map fst) proposed_modes, proposed_names = - map_filter - (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes, + the_default [] (Option.map (map_filter + (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes), show_steps = chk "show_steps", show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", @@ -176,7 +176,7 @@ val opt_modes = Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |-- - P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") [] + P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE val opt_expected_modes = Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |-- diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 19 10:49:43 2009 +0100 @@ -282,7 +282,7 @@ datatype options = Options of { expected_modes : (string * mode' list) option, - proposed_modes : (string * mode' list) list, + proposed_modes : (string * mode' list) option, proposed_names : ((string * mode') * string) list, show_steps : bool, show_proof_trace : bool, @@ -299,7 +299,7 @@ }; fun expected_modes (Options opt) = #expected_modes opt -fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name +fun proposed_modes (Options opt) = #proposed_modes opt fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode') (#proposed_names opt) (name, mode) @@ -318,7 +318,7 @@ val default_options = Options { expected_modes = NONE, - proposed_modes = [], + proposed_modes = NONE, proposed_names = [], show_steps = false, show_intermediate_results = false, diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 19 10:49:43 2009 +0100 @@ -82,10 +82,6 @@ ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); -(* reference to preprocessing of InductiveSet package *) - -val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*) - (** fundamentals **) (* syntactic operations *) @@ -417,22 +413,45 @@ end (* validity checks *) +(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *) -fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes = - case expected_modes options of - SOME (s, ms) => (case AList.lookup (op =) modes s of - SOME modes => - let - val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes - in - if not (eq_set eq_mode' (ms, modes')) then - error ("expected modes were not inferred:\n" - ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n" - ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms)) - else () - end - | NONE => ()) - | NONE => () +fun check_expected_modes preds options modes = + case expected_modes options of + SOME (s, ms) => (case AList.lookup (op =) modes s of + SOME modes => + let + val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes + in + if not (eq_set eq_mode' (ms, modes')) then + error ("expected modes were not inferred:\n" + ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n" + ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms)) + else () + end + | NONE => ()) + | NONE => () + +fun check_proposed_modes preds options modes extra_modes errors = + case proposed_modes options of + SOME (s, ms) => (case AList.lookup (op =) modes s of + SOME inferred_ms => + let + val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes)) + val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) inferred_ms + in + if not (eq_set eq_mode' (ms, modes')) then + error ("expected modes were not inferred:\n" + ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n" + ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms) ^ "\n" + ^ "For the following clauses, the following modes could not be inferred: " ^ "\n" + ^ cat_lines errors ^ + (if not (null preds_without_modes) then + "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes + else "")) + else () + end + | NONE => ()) + | NONE => () (* importing introduction rules *) @@ -584,13 +603,13 @@ let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val intros = ind_set_codegen_preproc thy + val intros = (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index val pred = nth (#preds result) index val nparams = length (Inductive.params_of (#raw_induct result)) - (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams + (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams (expand_tuples_elim pre_elim))*) val elim = (Drule.standard o Skip_Proof.make_thm thy) @@ -659,8 +678,8 @@ fun register_predicate (constname, pre_intros, pre_elim, nparams) thy = let (* preprocessing *) - val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros) - val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim) + val intros = map (preprocess_intro thy) pre_intros + val elim = preprocess_elim thy nparams pre_elim in if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map @@ -1042,21 +1061,34 @@ else NONE end; -fun print_failed_mode options thy modes p m rs i = +fun print_failed_mode options thy modes p m rs is = if show_mode_inference options then let - val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ - p ^ " violates mode " ^ string_of_mode thy p m) + val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ + p ^ " violates mode " ^ string_of_mode thy p m) in () end else () +fun error_of thy p m is = + (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^ + p ^ " violates mode " ^ string_of_mode thy p m) + +fun find_indices f xs = + map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs) + fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = let val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] - in (p, filter (fn m => case find_index - (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of - ~1 => true - | i => (print_failed_mode options thy modes p m rs i; false)) ms) + fun invalid_mode m = + case find_indices + (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of + [] => NONE + | is => SOME (error_of thy p m is) + val res = map (fn m => (m, invalid_mode m)) ms + val ms' = map_filter (fn (m, NONE) => SOME m | _ => NONE) res + val errors = map_filter snd res + in + ((p, ms'), errors) end; fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) = @@ -1071,14 +1103,24 @@ let val y = f x in if x = y then x else fixp f y end; +fun fixp_with_state f ((x : (string * mode list) list), state) = + let + val (y, state') = f (x, state) + in + if x = y then (y, state') else fixp_with_state f (y, state') + end + fun infer_modes options thy extra_modes all_modes param_vs clauses = let - val modes = - fixp (fn modes => - map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes) - all_modes + val (modes, errors) = + fixp_with_state (fn (modes, errors) => + let + val res = map + (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes + in (map fst res, errors @ maps snd res) end) + (all_modes, []) in - map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes + (map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes, errors) end; fun remove_from rem [] = [] @@ -1087,7 +1129,7 @@ NONE => (k, vs) | SOME vs' => (k, subtract (op =) vs' vs)) :: remove_from rem xs - + fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses = let val prednames = map fst clauses @@ -1096,16 +1138,21 @@ |> filter_out (fn (name, _) => member (op =) prednames name) val starting_modes = remove_from extra_modes' all_modes fun eq_mode (m1, m2) = (m1 = m2) - val modes = - fixp (fn modes => - map (check_modes_pred options true thy param_vs clauses extra_modes' - (gen_modes @ modes)) modes) starting_modes + val (modes, errors) = + fixp_with_state (fn (modes, errors) => + let + val res = map + (check_modes_pred options true thy param_vs clauses extra_modes' + (gen_modes @ modes)) modes + in (map fst res, errors @ maps snd res) end) (starting_modes, []) + val moded_clauses = + map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes + val (moded_clauses', _) = infer_modes options thy extra_modes all_modes param_vs clauses + val join_moded_clauses_table = AList.join (op =) + (fn _ => fn ((mps1, mps2)) => + merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2)) in - AList.join (op =) - (fn _ => fn ((mps1, mps2)) => - merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2)) - (infer_modes options thy extra_modes all_modes param_vs clauses, - map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes) + (join_moded_clauses_table (moded_clauses', moded_clauses), errors) end; (* term construction *) @@ -1524,66 +1571,67 @@ let val compfuns = PredicateCompFuns.compfuns val T = AList.lookup (op =) preds name |> the - fun create_definition (mode as (iss, is)) thy = let - val mode_cname = create_constname_of_mode options thy "" name T mode - val mode_cbasename = Long_Name.base_name mode_cname - val Ts = binder_types T - val (Ts1, Ts2) = chop (length iss) Ts - val (Us1, Us2) = split_smodeT is Ts2 - val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1 - val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2)) - val names = Name.variant_list [] - (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); - val param_names = Name.variant_list [] - (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1'))) - val xparams = map2 (curry Free) param_names Ts1' - fun mk_vars (i, T) names = - let - val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i)) - in - case AList.lookup (op =) is i of - NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names) - | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names) - | SOME (SOME pis) => - let - val (Tins, Touts) = split_tupleT pis T - val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in") - val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out") - val xin = Free (name_in, HOLogic.mk_tupleT Tins) - val xout = Free (name_out, HOLogic.mk_tupleT Touts) - val xarg = mk_arg xin xout pis T - in - (((if null Tins then [] else [xin], - if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end - end - val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names - val (xinout, xargs) = split_list xinoutargs - val (xins, xouts) = pairself flat (split_list xinout) - val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names - fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t - | mk_split_lambda [x] t = lambda x t - | mk_split_lambda xs t = - let - fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) - | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) - in - mk_split_lambda' xs t + fun create_definition (mode as (iss, is)) thy = + let + val mode_cname = create_constname_of_mode options thy "" name T mode + val mode_cbasename = Long_Name.base_name mode_cname + val Ts = binder_types T + val (Ts1, Ts2) = chop (length iss) Ts + val (Us1, Us2) = split_smodeT is Ts2 + val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1 + val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2)) + val names = Name.variant_list [] + (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); + val param_names = Name.variant_list [] + (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1'))) + val xparams = map2 (curry Free) param_names Ts1' + fun mk_vars (i, T) names = + let + val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i)) + in + case AList.lookup (op =) is i of + NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names) + | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names) + | SOME (SOME pis) => + let + val (Tins, Touts) = split_tupleT pis T + val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in") + val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out") + val xin = Free (name_in, HOLogic.mk_tupleT Tins) + val xout = Free (name_out, HOLogic.mk_tupleT Touts) + val xarg = mk_arg xin xout pis T + in + (((if null Tins then [] else [xin], + if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end + end + val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names + val (xinout, xargs) = split_list xinoutargs + val (xins, xouts) = pairself flat (split_list xinout) + val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names + fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t + | mk_split_lambda [x] t = lambda x t + | mk_split_lambda xs t = + let + fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) + | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) + in + mk_split_lambda' xs t + end; + val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts + (list_comb (Const (name, T), xparams' @ xargs))) + val lhs = list_comb (Const (mode_cname, funT), xparams @ xins) + val def = Logic.mk_equals (lhs, predterm) + val ([definition], thy') = thy |> + Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> + PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] + val (intro, elim) = + create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy' + in thy' + |> add_predfun name mode (mode_cname, definition, intro, elim) + |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd + |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd + |> Theory.checkpoint end; - val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts - (list_comb (Const (name, T), xparams' @ xargs))) - val lhs = list_comb (Const (mode_cname, funT), xparams @ xins) - val def = Logic.mk_equals (lhs, predterm) - val ([definition], thy') = thy |> - Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> - PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] - val (intro, elim) = - create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy' - in thy' - |> add_predfun name mode (mode_cname, definition, intro, elim) - |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd - |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd - |> Theory.checkpoint - end; in fold create_definition modes thy end; @@ -1626,8 +1674,8 @@ (* MAJOR FIXME: prove_params should be simple - different form of introrule for parameters ? *) -fun prove_param thy NONE t = TRY (rtac @{thm refl} 1) - | prove_param thy (m as SOME (Mode (mode, is, ms))) t = +fun prove_param options thy NONE t = TRY (rtac @{thm refl} 1) + | prove_param options thy (m as SOME (Mode (mode, is, ms))) t = let val (f, args) = strip_comb (Envir.eta_contract t) val (params, _) = chop (length ms) args @@ -1639,16 +1687,15 @@ | Free _ => TRY (rtac @{thm refl} 1) | Abs _ => error "prove_param: No valid parameter term" in - REPEAT_DETERM (etac @{thm thin_rl} 1) - THEN REPEAT_DETERM (rtac @{thm ext} 1) - THEN print_tac "prove_param" + REPEAT_DETERM (rtac @{thm ext} 1) + THEN print_tac' options "prove_param" THEN f_tac - THEN print_tac "after simplification in prove_args" - THEN (EVERY (map2 (prove_param thy) ms params)) + THEN print_tac' options "after simplification in prove_args" + THEN (EVERY (map2 (prove_param options thy) ms params)) THEN (REPEAT_DETERM (atac 1)) end -fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) = +fun prove_expr options thy (Mode (mode, is, ms), t, us) (premposition : int) = case strip_comb t of (Const (name, T), args) => let @@ -1656,16 +1703,16 @@ val (args1, args2) = chop (length ms) args in rtac @{thm bindI} 1 - THEN print_tac "before intro rule:" + THEN print_tac' options "before intro rule:" (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule) THEN rtac introrule 1 - THEN print_tac "after intro rule" + THEN print_tac' options "after intro rule" (* work with parameter arguments *) - THEN (atac 1) - THEN (print_tac "parameter goal") - THEN (EVERY (map2 (prove_param thy) ms args1)) + THEN atac 1 + THEN print_tac' options "parameter goal" + THEN (EVERY (map2 (prove_param options thy) ms args1)) THEN (REPEAT_DETERM (atac 1)) end | _ => rtac @{thm bindI} 1 @@ -1673,7 +1720,7 @@ (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1 THEN (atac 1) - THEN print_tac "after prove parameter call" + THEN print_tac' options "after prove parameter call" fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; @@ -1725,9 +1772,9 @@ val (in_ts, clause_out_ts) = split_smode is ts; fun prove_prems out_ts [] = (prove_match thy out_ts) - THEN print_tac "before simplifying assumptions" + THEN print_tac' options "before simplifying assumptions" THEN asm_full_simp_tac HOL_basic_ss' 1 - THEN print_tac "before single intro rule" + THEN print_tac' options "before single intro rule" THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) = let @@ -1737,11 +1784,11 @@ val (_, out_ts''') = split_smode is us val rec_tac = prove_prems out_ts''' ps in - print_tac "before clause:" + print_tac' options "before clause:" THEN asm_simp_tac HOL_basic_ss 1 - THEN print_tac "before prove_expr:" - THEN prove_expr thy (mode, t, us) premposition - THEN print_tac "after prove_expr:" + THEN print_tac' options "before prove_expr:" + THEN prove_expr options thy (mode, t, us) premposition + THEN print_tac' options "after prove_expr:" THEN rec_tac end | Negprem (us, t) => @@ -1752,13 +1799,18 @@ val (_, params) = strip_comb t in rtac @{thm bindI} 1 + THEN print_tac' options "before prove_neg_expr:" THEN (if (is_some name) then - simp_tac (HOL_basic_ss addsimps + print_tac' options ("before unfolding definition " ^ + (Display.string_of_thm_global thy + (predfun_definition_of thy (the name) (iss, is)))) + THEN simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 THEN rtac @{thm not_predI} 1 + THEN print_tac' options "after applying rule not_predI" THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN (REPEAT_DETERM (atac 1)) - THEN (EVERY (map2 (prove_param thy) param_modes params)) + THEN (EVERY (map2 (prove_param options thy) param_modes params)) else rtac @{thm not_predI'} 1) THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 @@ -1767,9 +1819,9 @@ | Sidecond t => rtac @{thm bindI} 1 THEN rtac @{thm if_predI} 1 - THEN print_tac "before sidecond:" + THEN print_tac' options "before sidecond:" THEN prove_sidecond thy modes t - THEN print_tac "after sidecond:" + THEN print_tac' options "after sidecond:" THEN prove_prems [] ps) in (prove_match thy out_ts) THEN rest_tac @@ -1800,7 +1852,7 @@ (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses)) - THEN print_tac "proved one direction" + THEN print_tac' options "proved one direction" end; (** Proof in the other direction **) @@ -2106,9 +2158,10 @@ map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us) end val all_modes = map (fn (s, T) => - case proposed_modes options s of + case proposed_modes options of NONE => (s, modes_of_typ T) - | SOME modes' => (s, map (translate_mode' nparams) modes')) + | SOME (s', modes') => + if s = s' then (s, map (translate_mode' nparams) modes') else (s, modes_of_typ T)) preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; @@ -2173,12 +2226,12 @@ val args = map2 (curry Free) arg_names Ts val predfun = Const (predfun_name_of thy predname full_mode, Ts ---> PredicateCompFuns.mk_predT @{typ unit}) - val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"}) + val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) val eq_term = HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) val def = predfun_definition_of thy predname full_mode val tac = fn _ => Simplifier.simp_tac - (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1 + (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1 val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac in (pred, result_thms @ [eq]) @@ -2199,7 +2252,7 @@ define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory, infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list - -> moded_clause list pred_mode_table, + -> moded_clause list pred_mode_table * string list, prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list -> (string * mode list) list -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, @@ -2220,10 +2273,11 @@ val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = prepare_intrs options thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." - val moded_clauses = + val (moded_clauses, errors) = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes preds options modes + val _ = check_proposed_modes preds options modes extra_modes errors val _ = print_modes options thy modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 10:49:43 2009 +0100 @@ -137,7 +137,7 @@ th' end -fun store_thm_in_table options ignore_consts thy th= +fun store_thm_in_table options ignore thy th= let val th = th |> inline_equations options thy @@ -153,29 +153,29 @@ else if (is_introlike th) then (defining_const_of_introrule th, th) else error "store_thm: unexpected definition format" in - if not (member (op =) ignore_consts const) then - Symtab.cons_list (const, th) - else I + if ignore const then I else Symtab.cons_list (const, th) end fun make_const_spec_table options thy = let - fun store ignore_const f = - fold (store_thm_in_table options ignore_const thy) + fun store ignore f = + fold (store_thm_in_table options ignore thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) val table = Symtab.empty - |> store [] Predicate_Compile_Alternative_Defs.get - val ignore_consts = Symtab.keys table + |> store (K false) Predicate_Compile_Alternative_Defs.get + val ignore = Symtab.defined table in table - |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get - |> store ignore_consts Nitpick_Simps.get - |> store ignore_consts Nitpick_Intros.get + |> store ignore (fn ctxt => maps + (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else []) + (Spec_Rules.get ctxt)) + |> store ignore Nitpick_Simps.get + |> store ignore Nitpick_Intros.get end fun get_specification table constname = case Symtab.lookup table constname of - SOME thms => thms + SOME thms => thms | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") val logic_operator_names = diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 19 10:49:43 2009 +0100 @@ -89,9 +89,7 @@ fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t | mk_param thy lookup_pred t = - let - val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t)) - in if Predicate_Compile_Aux.is_predT (fastype_of t) then + if Predicate_Compile_Aux.is_predT (fastype_of t) then t else let @@ -109,7 +107,7 @@ val pred_body = HOLogic.mk_eq (body', resvar) val param = fold_rev lambda (vs' @ [resvar]) pred_body in param end - end + (* creates the list of premises for every intro rule *) (* theory -> term -> (string list, term list list) *) diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 10:49:43 2009 +0100 @@ -23,7 +23,7 @@ val options = Options { expected_modes = NONE, - proposed_modes = [], + proposed_modes = NONE, proposed_names = [], show_steps = true, show_intermediate_results = true, @@ -83,7 +83,7 @@ val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac val _ = tracing (Display.string_of_thm ctxt' intro) val thy'' = thy' - |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) + |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) |> Predicate_Compile.preprocess options full_constname |> Predicate_Compile_Core.add_equations options [full_constname] (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/Tools/primrec.ML Thu Nov 19 10:49:43 2009 +0100 @@ -198,7 +198,7 @@ (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1)))) val rhs = singleton (Syntax.check_terms ctxt) (TypeInfer.constrain varT raw_rhs); - in (var, ((Binding.name def_name, []), rhs)) end; + in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end; (* find datatypes which contain all datatypes in tnames' *) diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 19 10:33:20 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 19 10:49:43 2009 +0100 @@ -87,6 +87,9 @@ values "{(c, a, b). JamesBond a b c}" values "{(c, b, a). JamesBond a b c}" +values "{(a, b). JamesBond 0 b a}" +values "{(c, a). JamesBond a 0 c}" +values "{(a, c). JamesBond a 0 c}" subsection {* Alternative Rules *} @@ -476,6 +479,8 @@ subsection {* transitive predicate *} +text {* Also look at the tabled transitive closure in the Library *} + code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool, (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp @@ -509,6 +514,28 @@ values [mode: o => i => bool] 10 "{n. tranclp succ n 10}" values 20 "{(n, m). tranclp succ n m}" +inductive example_graph :: "int => int => bool" +where + "example_graph 0 1" +| "example_graph 1 2" +| "example_graph 1 3" +| "example_graph 4 7" +| "example_graph 4 5" +| "example_graph 5 6" +| "example_graph 7 6" +| "example_graph 7 8" + +inductive not_reachable_in_example_graph :: "int => int => bool" +where "\ (tranclp example_graph x y) ==> not_reachable_in_example_graph x y" + +code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph . + +thm not_reachable_in_example_graph.equation + +value "not_reachable_in_example_graph 0 3" +value "not_reachable_in_example_graph 4 8" +value "not_reachable_in_example_graph 5 6" + subsection {* IMP *} types @@ -724,7 +751,7 @@ subsection {* Inverting list functions *} -code_pred [inductify, show_intermediate_results] length . +code_pred [inductify] length . code_pred [inductify, random] length . thm size_listP.equation thm size_listP.random_equation @@ -804,8 +831,6 @@ thm spliceP.equation values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}" -(* TODO: correct error messages:*) -(* values {(xs, ys, zs). spliceP xs ... } *) code_pred [inductify] List.rev . code_pred [inductify] map . @@ -965,13 +990,8 @@ | objaddr: "\ Env conf n = i \ \ eval_var (ObjAddr n) conf (IntVal i)" | plus: "\ eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \ \ eval_var (Add l r) conf (IntVal (vl+vr))" -(* TODO: breaks if code_pred_intro is used? *) -(* -lemmas [code_pred_intro] = irconst objaddr plus -*) -thm eval_var.cases -code_pred eval_var . (*by (rule eval_var.cases)*) +code_pred eval_var . thm eval_var.equation values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\x. 0)|) val}" diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/Pure/Isar/code.ML Thu Nov 19 10:49:43 2009 +0100 @@ -775,49 +775,4 @@ end; -(** datastructure to log definitions for preprocessing of the predicate compiler **) -(* obviously a clone of Named_Thms *) - -signature PREDICATE_COMPILE_PREPROC_CONST_DEFS = -sig - val get: Proof.context -> thm list - val add_thm: thm -> Context.generic -> Context.generic - val del_thm: thm -> Context.generic -> Context.generic - - val add_attribute : attribute - val del_attribute : attribute - - val add_attrib : Attrib.src - - val setup: theory -> theory -end; - -structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS = -struct - -structure Data = Generic_Data -( - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; -); - -val get = Data.get o Context.Proof; - -val add_thm = Data.map o Thm.add_thm; -val del_thm = Data.map o Thm.del_thm; - -val add_attribute = Thm.declaration_attribute add_thm; -val del_attribute = Thm.declaration_attribute del_thm; - -val add_attrib = Attrib.internal (K add_attribute) - -val setup = - Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute) - ("declaration of definition for preprocessing of the predicate compiler") #> - PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get); - -end; - structure Code : CODE = struct open Code; end; diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/Pure/Isar/constdefs.ML Thu Nov 19 10:49:43 2009 +0100 @@ -55,8 +55,7 @@ |> PureThy.add_defs false [((name, def), atts)] |-> (fn [thm] => (* FIXME thm vs. atts !? *) Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #> - Code.add_default_eqn thm #> - Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm)); + Code.add_default_eqn thm); in ((c, T), thy') end; fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = diff -r 7ead0ccf6cbd -r bc75dbbbf3e6 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Nov 19 10:33:20 2009 +0100 +++ b/src/Pure/Isar/specification.ML Thu Nov 19 10:49:43 2009 +0100 @@ -212,8 +212,7 @@ val ([(def_name, [th'])], lthy4) = lthy3 |> Local_Theory.notes_kind Thm.definitionK - [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: - Code.add_default_eqn_attrib :: atts), [([th], [])])]; + [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; val _ =