66 val add_new_random_dseq_equations : options -> string list -> theory -> theory |
66 val add_new_random_dseq_equations : options -> string list -> theory -> theory |
67 val mk_tracing : string -> term -> term |
67 val mk_tracing : string -> term -> term |
68 val prepare_intrs : options -> Proof.context -> string list -> thm list -> |
68 val prepare_intrs : options -> Proof.context -> string list -> thm list -> |
69 ((string * typ) list * string list * string list * (string * mode list) list * |
69 ((string * typ) list * string list * string list * (string * mode list) list * |
70 (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list) |
70 (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list) |
71 type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool} |
71 type mode_analysis_options = |
|
72 {use_generators : bool, |
|
73 reorder_premises : bool, |
|
74 infer_pos_and_neg_modes : bool} |
72 datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode |
75 datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode |
73 | Mode_Pair of mode_derivation * mode_derivation | Term of mode |
76 | Mode_Pair of mode_derivation * mode_derivation | Term of mode |
74 val head_mode_of : mode_derivation -> mode |
77 val head_mode_of : mode_derivation -> mode |
75 type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list |
78 type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list |
76 type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list |
79 type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list |
1050 | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers |
1053 | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers |
1051 | c => comp_modifiers) |
1054 | c => comp_modifiers) |
1052 |
1055 |
1053 (** mode analysis **) |
1056 (** mode analysis **) |
1054 |
1057 |
1055 type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool} |
1058 type mode_analysis_options = |
|
1059 {use_generators : bool, |
|
1060 reorder_premises : bool, |
|
1061 infer_pos_and_neg_modes : bool} |
1056 |
1062 |
1057 fun is_constrt thy = |
1063 fun is_constrt thy = |
1058 let |
1064 let |
1059 val cnstrs = flat (maps |
1065 val cnstrs = flat (maps |
1060 (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
1066 (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
1409 (case |
1415 (case |
1410 (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of |
1416 (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of |
1411 SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd |
1417 SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd |
1412 (known_vs_after p vs) (filter_out (equal p) ps) |
1418 (known_vs_after p vs) (filter_out (equal p) ps) |
1413 | SOME (p, SOME (deriv, missing_vars)) => |
1419 | SOME (p, SOME (deriv, missing_vars)) => |
1414 if #use_random mode_analysis_options andalso pol then |
1420 if #use_generators mode_analysis_options andalso pol then |
1415 check_mode_prems ((p, deriv) :: (map |
1421 check_mode_prems ((p, deriv) :: (map |
1416 (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) |
1422 (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) |
1417 (distinct (op =) missing_vars)) |
1423 (distinct (op =) missing_vars)) |
1418 @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps) |
1424 @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps) |
1419 else NONE |
1425 else NONE |
1424 NONE => NONE |
1430 NONE => NONE |
1425 | SOME (acc_ps, vs, rnd) => |
1431 | SOME (acc_ps, vs, rnd) => |
1426 if forall (is_constructable vs) (in_ts @ out_ts) then |
1432 if forall (is_constructable vs) (in_ts @ out_ts) then |
1427 SOME (ts, rev acc_ps, rnd) |
1433 SOME (ts, rev acc_ps, rnd) |
1428 else |
1434 else |
1429 if #use_random mode_analysis_options andalso pol then |
1435 if #use_generators mode_analysis_options andalso pol then |
1430 let |
1436 let |
1431 val generators = map |
1437 val generators = map |
1432 (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) |
1438 (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output)) |
1433 (subtract (op =) vs (terms_vs (in_ts @ out_ts))) |
1439 (subtract (op =) vs (terms_vs (in_ts @ out_ts))) |
1434 in |
1440 in |
2794 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 |
2795 -> 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, |
2796 add_code_equations : Proof.context -> (string * typ) list |
2802 add_code_equations : Proof.context -> (string * typ) list |
2797 -> (string * thm list) list -> (string * thm list) list, |
2803 -> (string * thm list) list -> (string * thm list) list, |
2798 comp_modifiers : Comp_Mod.comp_modifiers, |
2804 comp_modifiers : Comp_Mod.comp_modifiers, |
2799 use_random : bool, |
2805 use_generators : bool, |
2800 qname : bstring |
2806 qname : bstring |
2801 } |
2807 } |
2802 |
2808 |
2803 fun add_equations_of steps mode_analysis_options options prednames thy = |
2809 fun add_equations_of steps mode_analysis_options options prednames thy = |
2804 let |
2810 let |
2905 val thy'' = fold preprocess (flat scc) thy' |
2911 val thy'' = fold preprocess (flat scc) thy' |
2906 val thy''' = fold_rev |
2912 val thy''' = fold_rev |
2907 (fn preds => fn thy => |
2913 (fn preds => fn thy => |
2908 if not (forall (defined (ProofContext.init_global thy)) preds) then |
2914 if not (forall (defined (ProofContext.init_global thy)) preds) then |
2909 let |
2915 let |
2910 val mode_analysis_options = {use_random = #use_random (dest_steps steps), |
2916 val mode_analysis_options = {use_generators = #use_generators (dest_steps steps), |
2911 reorder_premises = |
2917 reorder_premises = |
2912 not (no_topmost_reordering options andalso not (null (inter (op =) preds names))), |
2918 not (no_topmost_reordering options andalso not (null (inter (op =) preds names))), |
2913 infer_pos_and_neg_modes = #use_random (dest_steps steps)} |
2919 infer_pos_and_neg_modes = #use_generators (dest_steps steps)} |
2914 in |
2920 in |
2915 add_equations_of steps mode_analysis_options options preds thy |
2921 add_equations_of steps mode_analysis_options options preds thy |
2916 end |
2922 end |
2917 else thy) |
2923 else thy) |
2918 scc thy'' |> Theory.checkpoint |
2924 scc thy'' |> Theory.checkpoint |
2925 create_definitions |
2931 create_definitions |
2926 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2932 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2927 prove = prove, |
2933 prove = prove, |
2928 add_code_equations = add_code_equations, |
2934 add_code_equations = add_code_equations, |
2929 comp_modifiers = predicate_comp_modifiers, |
2935 comp_modifiers = predicate_comp_modifiers, |
2930 use_random = false, |
2936 use_generators = false, |
2931 qname = "equation"}) |
2937 qname = "equation"}) |
2932 |
2938 |
2933 val add_depth_limited_equations = gen_add_equations |
2939 val add_depth_limited_equations = gen_add_equations |
2934 (Steps { |
2940 (Steps { |
2935 define_functions = |
2941 define_functions = |
2937 define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns |
2943 define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns |
2938 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2944 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2939 prove = prove_by_skip, |
2945 prove = prove_by_skip, |
2940 add_code_equations = K (K I), |
2946 add_code_equations = K (K I), |
2941 comp_modifiers = depth_limited_comp_modifiers, |
2947 comp_modifiers = depth_limited_comp_modifiers, |
2942 use_random = false, |
2948 use_generators = false, |
2943 qname = "depth_limited_equation"}) |
2949 qname = "depth_limited_equation"}) |
2944 |
2950 |
2945 val add_annotated_equations = gen_add_equations |
2951 val add_annotated_equations = gen_add_equations |
2946 (Steps { |
2952 (Steps { |
2947 define_functions = |
2953 define_functions = |
2949 define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds |
2955 define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds |
2950 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2956 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2951 prove = prove_by_skip, |
2957 prove = prove_by_skip, |
2952 add_code_equations = K (K I), |
2958 add_code_equations = K (K I), |
2953 comp_modifiers = annotated_comp_modifiers, |
2959 comp_modifiers = annotated_comp_modifiers, |
2954 use_random = false, |
2960 use_generators = false, |
2955 qname = "annotated_equation"}) |
2961 qname = "annotated_equation"}) |
2956 |
2962 |
2957 val add_random_equations = gen_add_equations |
2963 val add_random_equations = gen_add_equations |
2958 (Steps { |
2964 (Steps { |
2959 define_functions = |
2965 define_functions = |
2961 define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds |
2967 define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds |
2962 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2968 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2963 comp_modifiers = random_comp_modifiers, |
2969 comp_modifiers = random_comp_modifiers, |
2964 prove = prove_by_skip, |
2970 prove = prove_by_skip, |
2965 add_code_equations = K (K I), |
2971 add_code_equations = K (K I), |
2966 use_random = true, |
2972 use_generators = true, |
2967 qname = "random_equation"}) |
2973 qname = "random_equation"}) |
2968 |
2974 |
2969 val add_depth_limited_random_equations = gen_add_equations |
2975 val add_depth_limited_random_equations = gen_add_equations |
2970 (Steps { |
2976 (Steps { |
2971 define_functions = |
2977 define_functions = |
2973 define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds |
2979 define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds |
2974 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2980 (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2975 comp_modifiers = depth_limited_random_comp_modifiers, |
2981 comp_modifiers = depth_limited_random_comp_modifiers, |
2976 prove = prove_by_skip, |
2982 prove = prove_by_skip, |
2977 add_code_equations = K (K I), |
2983 add_code_equations = K (K I), |
2978 use_random = true, |
2984 use_generators = true, |
2979 qname = "depth_limited_random_equation"}) |
2985 qname = "depth_limited_random_equation"}) |
2980 |
2986 |
2981 val add_dseq_equations = gen_add_equations |
2987 val add_dseq_equations = gen_add_equations |
2982 (Steps { |
2988 (Steps { |
2983 define_functions = |
2989 define_functions = |
2985 define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns |
2991 define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns |
2986 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2992 options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), |
2987 prove = prove_by_skip, |
2993 prove = prove_by_skip, |
2988 add_code_equations = K (K I), |
2994 add_code_equations = K (K I), |
2989 comp_modifiers = dseq_comp_modifiers, |
2995 comp_modifiers = dseq_comp_modifiers, |
2990 use_random = false, |
2996 use_generators = false, |
2991 qname = "dseq_equation"}) |
2997 qname = "dseq_equation"}) |
2992 |
2998 |
2993 val add_random_dseq_equations = gen_add_equations |
2999 val add_random_dseq_equations = gen_add_equations |
2994 (Steps { |
3000 (Steps { |
2995 define_functions = |
3001 define_functions = |
3003 options preds (s, neg_modes) |
3009 options preds (s, neg_modes) |
3004 end, |
3010 end, |
3005 prove = prove_by_skip, |
3011 prove = prove_by_skip, |
3006 add_code_equations = K (K I), |
3012 add_code_equations = K (K I), |
3007 comp_modifiers = pos_random_dseq_comp_modifiers, |
3013 comp_modifiers = pos_random_dseq_comp_modifiers, |
3008 use_random = true, |
3014 use_generators = true, |
3009 qname = "random_dseq_equation"}) |
3015 qname = "random_dseq_equation"}) |
3010 |
3016 |
3011 val add_new_random_dseq_equations = gen_add_equations |
3017 val add_new_random_dseq_equations = gen_add_equations |
3012 (Steps { |
3018 (Steps { |
3013 define_functions = |
3019 define_functions = |
3021 options preds (s, neg_modes) |
3027 options preds (s, neg_modes) |
3022 end, |
3028 end, |
3023 prove = prove_by_skip, |
3029 prove = prove_by_skip, |
3024 add_code_equations = K (K I), |
3030 add_code_equations = K (K I), |
3025 comp_modifiers = new_pos_random_dseq_comp_modifiers, |
3031 comp_modifiers = new_pos_random_dseq_comp_modifiers, |
3026 use_random = true, |
3032 use_generators = true, |
3027 qname = "new_random_dseq_equation"}) |
3033 qname = "new_random_dseq_equation"}) |
3028 |
3034 |
3029 (** user interface **) |
3035 (** user interface **) |
3030 |
3036 |
3031 (* code_pred_intro attribute *) |
3037 (* code_pred_intro attribute *) |