24 val predfun_elim_of: Proof.context -> string -> mode -> thm |
24 val predfun_elim_of: Proof.context -> string -> mode -> thm |
25 val all_preds_of : Proof.context -> string list |
25 val all_preds_of : Proof.context -> string list |
26 val modes_of: compilation -> Proof.context -> string -> mode list |
26 val modes_of: compilation -> Proof.context -> string -> mode list |
27 val all_modes_of : compilation -> Proof.context -> (string * mode list) list |
27 val all_modes_of : compilation -> Proof.context -> (string * mode list) list |
28 val all_random_modes_of : Proof.context -> (string * mode list) list |
28 val all_random_modes_of : Proof.context -> (string * mode list) list |
29 val intros_of : theory -> string -> thm list |
29 val intros_of : Proof.context -> string -> thm list |
30 val add_intro : thm -> theory -> theory |
30 val add_intro : thm -> theory -> theory |
31 val set_elim : thm -> theory -> theory |
31 val set_elim : thm -> theory -> theory |
32 val register_alternative_function : string -> mode -> string -> theory -> theory |
32 val register_alternative_function : string -> mode -> string -> theory -> theory |
33 val alternative_compilation_of_global : theory -> string -> mode -> |
33 val alternative_compilation_of_global : theory -> string -> mode -> |
34 (compilation_funs -> typ -> term) option |
34 (compilation_funs -> typ -> term) option |
37 val functional_compilation : string -> mode -> compilation_funs -> typ -> term |
37 val functional_compilation : string -> mode -> compilation_funs -> typ -> term |
38 val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory |
38 val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory |
39 val force_modes_and_compilations : string -> |
39 val force_modes_and_compilations : string -> |
40 (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory |
40 (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory |
41 val preprocess_intro : theory -> thm -> thm |
41 val preprocess_intro : theory -> thm -> thm |
42 val print_stored_rules : theory -> unit |
42 val print_stored_rules : Proof.context -> unit |
43 val print_all_modes : compilation -> Proof.context -> unit |
43 val print_all_modes : compilation -> Proof.context -> unit |
44 val mk_casesrule : Proof.context -> term -> thm list -> term |
44 val mk_casesrule : Proof.context -> term -> thm list -> term |
45 val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref |
45 val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref |
46 val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) |
46 val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) |
47 option Unsynchronized.ref |
47 option Unsynchronized.ref |
228 val merge = Graph.merge eq_pred_data; |
228 val merge = Graph.merge eq_pred_data; |
229 ); |
229 ); |
230 |
230 |
231 (* queries *) |
231 (* queries *) |
232 |
232 |
233 fun lookup_pred_data thy name = |
233 fun lookup_pred_data ctxt name = |
234 Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) |
234 Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name) |
235 |
235 |
236 fun the_pred_data thy name = case lookup_pred_data thy name |
236 fun the_pred_data ctxt name = case lookup_pred_data ctxt name |
237 of NONE => error ("No such predicate " ^ quote name) |
237 of NONE => error ("No such predicate " ^ quote name) |
238 | SOME data => data; |
238 | SOME data => data; |
239 |
239 |
240 val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of |
240 val is_registered = is_some oo lookup_pred_data |
241 |
241 |
242 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of |
242 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of |
243 |
243 |
244 fun intros_of thy = #intros o the_pred_data thy |
244 val intros_of = #intros oo the_pred_data |
245 |
245 |
246 fun the_elim_of thy name = case #elim (the_pred_data thy name) |
246 fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name) |
247 of NONE => error ("No elimination rule for predicate " ^ quote name) |
247 of NONE => error ("No elimination rule for predicate " ^ quote name) |
248 | SOME thm => Thm.transfer thy thm |
248 | SOME thm => thm |
249 |
249 |
250 val has_elim = is_some o #elim oo the_pred_data; |
250 val has_elim = is_some o #elim oo the_pred_data |
251 |
251 |
252 fun function_names_of compilation ctxt name = |
252 fun function_names_of compilation ctxt name = |
253 case AList.lookup (op =) (#function_names (the_pred_data (ProofContext.theory_of ctxt) name)) compilation of |
253 case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of |
254 NONE => error ("No " ^ string_of_compilation compilation |
254 NONE => error ("No " ^ string_of_compilation compilation |
255 ^ "functions defined for predicate " ^ quote name) |
255 ^ "functions defined for predicate " ^ quote name) |
256 | SOME fun_names => fun_names |
256 | SOME fun_names => fun_names |
257 |
257 |
258 fun function_name_of compilation ctxt name mode = |
258 fun function_name_of compilation ctxt name mode = |
268 map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name)) |
268 map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name)) |
269 (all_preds_of ctxt) |
269 (all_preds_of ctxt) |
270 |
270 |
271 val all_random_modes_of = all_modes_of Random |
271 val all_random_modes_of = all_modes_of Random |
272 |
272 |
273 fun defined_functions compilation ctxt name = case lookup_pred_data (ProofContext.theory_of ctxt) name of |
273 fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of |
274 NONE => false |
274 NONE => false |
275 | SOME data => AList.defined (op =) (#function_names data) compilation |
275 | SOME data => AList.defined (op =) (#function_names data) compilation |
276 |
276 |
277 fun needs_random ctxt s m = |
277 fun needs_random ctxt s m = |
278 member (op =) (#needs_random (the_pred_data (ProofContext.theory_of ctxt) s)) m |
278 member (op =) (#needs_random (the_pred_data ctxt s)) m |
279 |
279 |
280 fun lookup_predfun_data thy name mode = |
280 fun lookup_predfun_data ctxt name mode = |
281 Option.map rep_predfun_data |
281 Option.map rep_predfun_data |
282 (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode) |
282 (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode) |
283 |
283 |
284 fun the_predfun_data thy name mode = |
284 fun the_predfun_data ctxt name mode = |
285 case lookup_predfun_data thy name mode of |
285 case lookup_predfun_data ctxt name mode of |
286 NONE => error ("No function defined for mode " ^ string_of_mode mode ^ |
286 NONE => error ("No function defined for mode " ^ string_of_mode mode ^ |
287 " of predicate " ^ name) |
287 " of predicate " ^ name) |
288 | SOME data => data; |
288 | SOME data => data; |
289 |
289 |
290 val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of |
290 val predfun_definition_of = #definition ooo the_predfun_data |
291 |
291 |
292 val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of |
292 val predfun_intro_of = #intro ooo the_predfun_data |
293 |
293 |
294 val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of |
294 val predfun_elim_of = #elim ooo the_predfun_data |
295 |
295 |
296 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of |
296 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data |
297 |
297 |
298 (* diagnostic display functions *) |
298 (* diagnostic display functions *) |
299 |
299 |
300 fun print_modes options modes = |
300 fun print_modes options modes = |
301 if show_modes options then |
301 if show_modes options then |
329 fun print_compiled_terms options ctxt = |
329 fun print_compiled_terms options ctxt = |
330 if show_compilation options then |
330 if show_compilation options then |
331 print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt) |
331 print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt) |
332 else K () |
332 else K () |
333 |
333 |
334 fun print_stored_rules thy = |
334 fun print_stored_rules ctxt = |
335 let |
335 let |
336 val preds = (Graph.keys o PredData.get) thy |
336 val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt)) |
337 fun print pred () = let |
337 fun print pred () = let |
338 val _ = writeln ("predicate: " ^ pred) |
338 val _ = writeln ("predicate: " ^ pred) |
339 val _ = writeln ("introrules: ") |
339 val _ = writeln ("introrules: ") |
340 val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm)) |
340 val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm)) |
341 (rev (intros_of thy pred)) () |
341 (rev (intros_of ctxt pred)) () |
342 in |
342 in |
343 if (has_elim thy pred) then |
343 if (has_elim ctxt pred) then |
344 writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred)) |
344 writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred)) |
345 else |
345 else |
346 writeln ("no elimrule defined") |
346 writeln ("no elimrule defined") |
347 end |
347 end |
348 in |
348 in |
349 fold print preds () |
349 fold print preds () |
611 |
611 |
612 fun expand_tuples_elim th = th |
612 fun expand_tuples_elim th = th |
613 |
613 |
614 val no_compilation = ([], ([], [])) |
614 val no_compilation = ([], ([], [])) |
615 |
615 |
616 fun fetch_pred_data thy name = |
616 fun fetch_pred_data ctxt name = |
617 case try (Inductive.the_inductive (ProofContext.init_global thy)) name of |
617 case try (Inductive.the_inductive ctxt) name of |
618 SOME (info as (_, result)) => |
618 SOME (info as (_, result)) => |
619 let |
619 let |
620 fun is_intro_of intro = |
620 fun is_intro_of intro = |
621 let |
621 let |
622 val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) |
622 val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) |
623 in (fst (dest_Const const) = name) end; |
623 in (fst (dest_Const const) = name) end; |
|
624 val thy = ProofContext.theory_of ctxt |
624 val intros = |
625 val intros = |
625 (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) |
626 (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) |
626 val index = find_index (fn s => s = name) (#names (fst info)) |
627 val index = find_index (fn s => s = name) (#names (fst info)) |
627 val pre_elim = nth (#elims result) index |
628 val pre_elim = nth (#elims result) index |
628 val pred = nth (#preds result) index |
629 val pred = nth (#preds result) index |
629 val nparams = length (Inductive.params_of (#raw_induct result)) |
630 val nparams = length (Inductive.params_of (#raw_induct result)) |
630 val ctxt = ProofContext.init_global thy |
|
631 val elim_t = mk_casesrule ctxt pred intros |
631 val elim_t = mk_casesrule ctxt pred intros |
632 val elim = |
632 val elim = |
633 prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t |
633 prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t |
634 in |
634 in |
635 mk_pred_data ((intros, SOME elim), no_compilation) |
635 mk_pred_data ((intros, SOME elim), no_compilation) |
2407 | select_sup _ 1 = [rtac @{thm supI1}] |
2407 | select_sup _ 1 = [rtac @{thm supI1}] |
2408 | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); |
2408 | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); |
2409 |
2409 |
2410 fun prove_one_direction options ctxt clauses preds pred mode moded_clauses = |
2410 fun prove_one_direction options ctxt clauses preds pred mode moded_clauses = |
2411 let |
2411 let |
2412 val thy = ProofContext.theory_of ctxt |
|
2413 val T = the (AList.lookup (op =) preds pred) |
2412 val T = the (AList.lookup (op =) preds pred) |
2414 val nargs = length (binder_types T) |
2413 val nargs = length (binder_types T) |
2415 val pred_case_rule = the_elim_of thy pred |
2414 val pred_case_rule = the_elim_of ctxt pred |
2416 in |
2415 in |
2417 REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) |
2416 REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) |
2418 THEN print_tac options "before applying elim rule" |
2417 THEN print_tac options "before applying elim rule" |
2419 THEN etac (predfun_elim_of ctxt pred mode) 1 |
2418 THEN etac (predfun_elim_of ctxt pred mode) 1 |
2420 THEN etac pred_case_rule 1 |
2419 THEN etac pred_case_rule 1 |
2517 THEN print_tac options "after sidecond2 simplification" |
2516 THEN print_tac options "after sidecond2 simplification" |
2518 end |
2517 end |
2519 |
2518 |
2520 fun prove_clause2 options ctxt pred mode (ts, ps) i = |
2519 fun prove_clause2 options ctxt pred mode (ts, ps) i = |
2521 let |
2520 let |
2522 val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1) |
2521 val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) |
2523 val (in_ts, clause_out_ts) = split_mode mode ts; |
2522 val (in_ts, clause_out_ts) = split_mode mode ts; |
2524 fun prove_prems2 out_ts [] = |
2523 fun prove_prems2 out_ts [] = |
2525 print_tac options "before prove_match2 - last call:" |
2524 print_tac options "before prove_match2 - last call:" |
2526 THEN prove_match2 options ctxt out_ts |
2525 THEN prove_match2 options ctxt out_ts |
2527 THEN print_tac options "after prove_match2 - last call:" |
2526 THEN print_tac options "after prove_match2 - last call:" |
2760 in forall check prednames end |
2759 in forall check prednames end |
2761 *) |
2760 *) |
2762 |
2761 |
2763 (* create code equation *) |
2762 (* create code equation *) |
2764 |
2763 |
2765 fun add_code_equations thy preds result_thmss = |
2764 fun add_code_equations ctxt preds result_thmss = |
2766 let |
2765 let |
2767 val ctxt = ProofContext.init_global thy |
|
2768 fun add_code_equation (predname, T) (pred, result_thms) = |
2766 fun add_code_equation (predname, T) (pred, result_thms) = |
2769 let |
2767 let |
2770 val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool |
2768 val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool |
2771 in |
2769 in |
2772 if member (op =) (modes_of Pred ctxt predname) full_mode then |
2770 if member (op =) (modes_of Pred ctxt predname) full_mode then |
2799 datatype steps = Steps of |
2797 datatype steps = Steps of |
2800 { |
2798 { |
2801 define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory, |
2799 define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory, |
2802 prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list |
2800 prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list |
2803 -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, |
2801 -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, |
2804 add_code_equations : theory -> (string * typ) list |
2802 add_code_equations : Proof.context -> (string * typ) list |
2805 -> (string * thm list) list -> (string * thm list) list, |
2803 -> (string * thm list) list -> (string * thm list) list, |
2806 comp_modifiers : Comp_Mod.comp_modifiers, |
2804 comp_modifiers : Comp_Mod.comp_modifiers, |
2807 use_random : bool, |
2805 use_random : bool, |
2808 qname : bstring |
2806 qname : bstring |
2809 } |
2807 } |
2810 |
2808 |
2811 fun add_equations_of steps mode_analysis_options options prednames thy = |
2809 fun add_equations_of steps mode_analysis_options options prednames thy = |
2812 let |
2810 let |
2813 fun dest_steps (Steps s) = s |
2811 fun dest_steps (Steps s) = s |
2814 val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) |
2812 val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) |
|
2813 val ctxt = ProofContext.init_global thy |
2815 val _ = print_step options |
2814 val _ = print_step options |
2816 ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation |
2815 ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation |
2817 ^ ") for predicates " ^ commas prednames ^ "...") |
2816 ^ ") for predicates " ^ commas prednames ^ "...") |
2818 (*val _ = check_intros_elim_match thy prednames*) |
2817 (*val _ = check_intros_elim_match thy prednames*) |
2819 (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) |
2818 (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) |
2820 val _ = |
2819 val _ = |
2821 if show_intermediate_results options then |
2820 if show_intermediate_results options then |
2822 tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) |
2821 tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames))) |
2823 else () |
2822 else () |
2824 val (preds, all_vs, param_vs, all_modes, clauses) = |
2823 val (preds, all_vs, param_vs, all_modes, clauses) = |
2825 prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames) |
2824 prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames) |
2826 val _ = print_step options "Infering modes..." |
2825 val _ = print_step options "Infering modes..." |
2827 val ((moded_clauses, errors), thy') = |
2826 val ((moded_clauses, errors), thy') = |
2828 Output.cond_timeit true "Infering modes" |
2827 Output.cond_timeit true "Infering modes" |
2829 (fn _ => infer_modes mode_analysis_options |
2828 (fn _ => infer_modes mode_analysis_options |
2830 options compilation preds all_modes param_vs clauses thy) |
2829 options compilation preds all_modes param_vs clauses thy) |
2846 val _ = print_compiled_terms options ctxt'' compiled_terms |
2845 val _ = print_compiled_terms options ctxt'' compiled_terms |
2847 val _ = print_step options "Proving equations..." |
2846 val _ = print_step options "Proving equations..." |
2848 val result_thms = |
2847 val result_thms = |
2849 Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => |
2848 Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => |
2850 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
2849 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
2851 val result_thms' = #add_code_equations (dest_steps steps) thy'' preds |
2850 val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds |
2852 (maps_modes result_thms) |
2851 (maps_modes result_thms) |
2853 val qname = #qname (dest_steps steps) |
2852 val qname = #qname (dest_steps steps) |
2854 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute |
2853 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute |
2855 (fn thm => Context.mapping (Code.add_eqn thm) I)))) |
2854 (fn thm => Context.mapping (Code.add_eqn thm) I)))) |
2856 val thy''' = |
2855 val thy''' = |
2881 let |
2880 let |
2882 fun dest_steps (Steps s) = s |
2881 fun dest_steps (Steps s) = s |
2883 val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) |
2882 val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) |
2884 val ctxt = ProofContext.init_global thy |
2883 val ctxt = ProofContext.init_global thy |
2885 val thy' = thy |
2884 val thy' = thy |
2886 |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of ctxt)) names) |
2885 |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) |
2887 |> Theory.checkpoint; |
2886 |> Theory.checkpoint; |
2888 fun strong_conn_of gr keys = |
2887 fun strong_conn_of gr keys = |
2889 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) |
2888 Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) |
2890 val scc = strong_conn_of (PredData.get thy') names |
2889 val scc = strong_conn_of (PredData.get thy') names |
2891 |
2890 |
3034 let |
3033 let |
3035 val thy = ProofContext.theory_of lthy |
3034 val thy = ProofContext.theory_of lthy |
3036 val const = prep_const thy raw_const |
3035 val const = prep_const thy raw_const |
3037 val ctxt = ProofContext.init_global thy |
3036 val ctxt = ProofContext.init_global thy |
3038 val lthy' = Local_Theory.theory (PredData.map |
3037 val lthy' = Local_Theory.theory (PredData.map |
3039 (extend (fetch_pred_data thy) (depending_preds_of ctxt) const)) lthy |
3038 (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy |
3040 val thy' = ProofContext.theory_of lthy' |
3039 val thy' = ProofContext.theory_of lthy' |
3041 val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy') |
3040 val ctxt' = ProofContext.init_global thy' |
|
3041 val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') |
3042 fun mk_cases const = |
3042 fun mk_cases const = |
3043 let |
3043 let |
3044 val T = Sign.the_const_type thy const |
3044 val T = Sign.the_const_type thy const |
3045 val pred = Const (const, T) |
3045 val pred = Const (const, T) |
3046 val intros = intros_of thy' const |
3046 val intros = intros_of ctxt' const |
3047 in mk_casesrule lthy' pred intros end |
3047 in mk_casesrule lthy' pred intros end |
3048 val cases_rules = map mk_cases preds |
3048 val cases_rules = map mk_cases preds |
3049 val cases = |
3049 val cases = |
3050 map (fn case_rule => Rule_Cases.Case {fixes = [], |
3050 map (fn case_rule => Rule_Cases.Case {fixes = [], |
3051 assumes = [("", Logic.strip_imp_prems case_rule)], |
3051 assumes = [("", Logic.strip_imp_prems case_rule)], |