1signature holfootLib = 2sig 3 include Abbrev 4 5 structure holfoot_param : sig 6 include Abbrev; 7 8 val combinator_thmL : thm list 9 val predicate_ssfrag : int -> simpLib.ssfrag 10 val final_decision_procedure : thm list -> term -> thm; 11 val combinator_terms : term * term * term; 12 val resource_proccall_free_thmL : thm list 13 val inital_prop_rewrite_thmL : thm list 14 val abstrL : separationLogicLib.asl_program_abstraction list 15 val comments_step_convL : (conv->conv) list 16 val quantifier_heuristicsL : quantHeuristicsLib.quant_param list 17 val var_res_prop_implies___GENERATE : 18 (term list -> int -> (bool * simpLib.ssfrag) -> thm list -> term * term * term * term -> thm list) list 19 20 val hoare_triple_case_splitL : (term -> term) list 21 val frame_split_case_splitL : (term -> term) list 22 23 structure var_res_base : sig 24 include Abbrev; 25 26 val var_res_prove : Abbrev.term -> Abbrev.thm 27 val var_res_prove___no_expn : Abbrev.term -> Abbrev.thm 28 val var_res_assumptions_prove : Abbrev.thm -> Abbrev.thm 29 val var_res_precondition_prove : Abbrev.thm -> Abbrev.thm 30 val var_res_precondition_assumption_prove : 31 Abbrev.term option -> Abbrev.thm -> Abbrev.thm 32 val raise_var_res_prove_expn : exn -> 'a 33 34 val COND_REWR_CONV : Abbrev.thm -> Abbrev.conv 35 val COND_REWRITE_CONV : bool -> Abbrev.thm list -> Abbrev.conv 36 val GUARDED_COND_REWRITE_CONV : bool -> (Abbrev.term -> bool) -> Abbrev.thm list -> Abbrev.conv 37 38 val VAR_RES_COND_HOARE_TRIPLE___PRECOND_CONV : conv -> conv 39 val VAR_RES_COND_HOARE_TRIPLE___FIRST_COMMAND___CONV : conv -> conv 40 val VAR_RES_COND_HOARE_TRIPLE___FIND_RESORT_PRECOND_CONV : (term -> bool) -> conv 41 42 val var_res_prop___VAR_EQ_PROPAGATE : conv 43 val VAR_RES_COND_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> (bool * term * thm) 44 val VAR_RES_COND_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm 45 val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_INTRO___CONV : term -> string option -> term -> thm 46 val VAR_RES_FRAME_SPLIT_INFERENCE___CONST_LIST_INTRO___CONV : (term * string option) list -> term -> thm 47 48 val var_res_prop_equal_unequal___NORMALISE_CONV : conv 49 val VAR_RES_PROP_REWRITE_CONV : (bool * simpLib.ssfrag) -> thm list -> term -> thm 50 val get_const_name_for_exp : string -> term -> string 51 52 val VAR_RES_COND_HOARE_TRIPLE___RESORT_PRECOND_CONV : int list -> conv 53 val var_res_prop___COND_RESORT_CONV : int list -> conv 54 55 val cond_rewrite___varlist_update : thm list -> conv 56 val GENERATE___var_res_exp_varlist_update___REWRITES : term -> term -> term -> (term * thm list) 57 val var_res_prop___var_res_prop_varlist_update___EVAL : term -> conv; 58 val VAR_RES_COND_INFERENCE___PRECOND_var_res_prop_varlist_update___EVAL : term -> conv 59 60 val BAG_NORMALISE_CONV : conv; 61 val VAR_RES_FRAME_SPLIT___imp_CONV : conv -> conv 62 val VAR_RES_FRAME_SPLIT___split_CONV : conv -> conv 63 val VAR_RES_FRAME_SPLIT___context_CONV : conv -> conv 64 val VAR_RES_FRAME_SPLIT___context_split_imp_CONV : conv -> conv 65 val VAR_RES_FRAME_SPLIT___PROP_CONV : conv -> conv 66 67 type var_res_inference_param = 68 {fast : bool, 69 do_prop_simps : bool, 70 prop_simp_ss : simpLib.ssfrag, 71 expands_level : int}; 72 73 type var_res_inference = var_res_inference_param -> thm list -> ConseqConv.directed_conseq_conv 74 75 val no_context_conseq_conv : ConseqConv.directed_conseq_conv -> var_res_inference; 76 val no_context_strengthen_conseq_conv : conv -> var_res_inference; 77 val context_strengthen_conseq_conv : (thm list -> conv) -> var_res_inference; 78 val simpset_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference; 79 val simpset_no_context_strengthen_conseq_conv : ((bool * simpLib.ssfrag) -> conv) -> var_res_inference; 80 val expands_strengthen_conseq_conv : (int -> (bool * simpLib.ssfrag) -> thm list -> conv) -> var_res_inference; 81 end 82 83 val INFERENCES_LIST___simulate_command : (string * var_res_base.var_res_inference) list 84 val INFERENCES_LIST___simulate_minor_command : (string * var_res_base.var_res_inference) list 85 val INFERENCES_LIST___expensive_simplifications : (string * var_res_base.var_res_inference) list 86 val INFERENCES_LIST___entailment_steps : (string * var_res_base.var_res_inference) list 87 88 val VAR_RES_IS_PURE_PROPOSITION___provers : (term -> term -> thm) list 89 end 90 91 structure holfoot_tactics : sig 92 type var_res_inference_group = 93 (* group name (used for debug) *) 94 string * 95 (* group guard, inferences are just applied to 96 terms that satisfy this guard *) 97 (Abbrev.term -> bool) * 98 (* apply before working on subterms *) 99 bool * 100 (* use this inference group to clean up after a "bigger" step *) 101 bool * 102 (* the members of the group, each with a name for debugging *) 103 (string * holfoot_param.var_res_base.var_res_inference) list; 104 105 type user_rewrite_param = (Abbrev.thm list * Abbrev.conv list * simpLib.ssfrag list); 106 type gen_step_param = {use_asms : bool, 107 do_case_splits : bool, 108 expands_level : int, 109 generate_vcs : bool, 110 fast : bool, 111 stop_evals : (Abbrev.term -> bool) list, 112 prop_simp_level: int, 113 inferences : (int * var_res_inference_group) list * 114 (int * var_res_inference_group) list * 115 (int * var_res_inference_group) list}; 116 117 datatype gen_step_tac_opt = 118 case_splits_flag of bool 119 | expands_level of int 120 | fast_flag of bool 121 | prop_simp_level of int 122 | use_asms_flag of bool 123 | generate_vcs_flag of bool 124 | add_rewrites of Abbrev.thm list 125 | add_convs of Abbrev.conv list 126 | add_ssfrags of simpLib.ssfrag list 127 | stop_evals of (Abbrev.term -> bool) list 128 | combined_gen_step_tac_opt of gen_step_tac_opt list 129 | add_inference_groups of (int * var_res_inference_group) list * 130 (int * var_res_inference_group) list * 131 (int * var_res_inference_group) list; 132 133 val no_case_splits : gen_step_tac_opt; 134 val do_case_splits : gen_step_tac_opt; 135 val no_expands : gen_step_tac_opt; 136 val do_expands : gen_step_tac_opt; 137 val full_expands : gen_step_tac_opt; 138 val no_case_split_expands : gen_step_tac_opt; 139 val generate_vcs : gen_step_tac_opt; 140 val dont_generate_vcs : gen_step_tac_opt; 141 val no_asms : gen_step_tac_opt; 142 val use_asms : gen_step_tac_opt; 143 val no_prop_simps : gen_step_tac_opt; 144 val simple_prop_simps : gen_step_tac_opt; 145 val conservative : gen_step_tac_opt; (* not fast *) 146 val careful : gen_step_tac_opt; (* no asms. no case splits, no expands *) 147 val stop_at_cond : gen_step_tac_opt; 148 val stop_at_while : gen_step_tac_opt; 149 val stop_at_abstraction : gen_step_tac_opt; 150 val stop_at_frame_calc : gen_step_tac_opt; 151 val stop_at_hoare_triple : gen_step_tac_opt; 152 val stop_at_block_spec : gen_step_tac_opt; 153 154 val gen_step_param___update_use_asms : gen_step_param -> bool -> gen_step_param 155 val gen_step_param___update_cs : gen_step_param -> bool -> gen_step_param 156 val gen_step_param___update_vcs : gen_step_param -> bool -> gen_step_param 157 val gen_step_param___update_expands : gen_step_param -> int -> gen_step_param 158 val gen_step_param___update_fast : gen_step_param -> bool -> gen_step_param 159 val gen_step_param___update_prop_simps : gen_step_param -> int -> gen_step_param 160 val gen_step_param___update_stop_evals : gen_step_param -> (Abbrev.term -> bool) list -> gen_step_param 161 val gen_step_param___update_inferences : gen_step_param -> ( 162 (int * var_res_inference_group) list * 163 (int * var_res_inference_group) list * 164 (int * var_res_inference_group) list) -> gen_step_param 165 166 val gen_step_param___add_inferences : gen_step_param -> ( 167 (int * var_res_inference_group) list * 168 (int * var_res_inference_group) list * 169 (int * var_res_inference_group) list) -> gen_step_param 170 171 val VAR_RES_GEN_STEP_CONSEQ_CONV : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv 172 val VAR_RES_GEN_STEP_TAC : gen_step_param -> user_rewrite_param -> int option -> int -> Abbrev.tactic 173 val xVAR_RES_GEN_STEP_CONSEQ_CONV: gen_step_tac_opt list -> int option -> int -> Abbrev.conv 174 val xVAR_RES_GEN_STEP_TAC : gen_step_tac_opt list -> int option -> int -> Abbrev.tactic 175 176 val VAR_RES_PURE_VC_TAC : Abbrev.tactic; 177 val VAR_RES_ELIM_COMMENTS_TAC : Abbrev.tactic 178 val VAR_RES_VC_TAC : Abbrev.tactic; 179 val VAR_RES_SPECIFICATION___CONSEQ_CONV : ConseqConv.conseq_conv 180 val VAR_RES_SPECIFICATION_TAC : Abbrev.tactic 181 val VAR_RES_ENTAILMENT_INIT___CONSEQ_CONV : ConseqConv.conseq_conv 182 val VAR_RES_ENTAILMENT_INIT_TAC : Abbrev.tactic 183end 184 185 186 val add_rewrites : Abbrev.thm list -> holfoot_tactics.gen_step_tac_opt; 187 val add_convs : Abbrev.conv list -> holfoot_tactics.gen_step_tac_opt; 188 val add_ssfrags : simpLib.ssfrag list -> holfoot_tactics.gen_step_tac_opt; 189 val combined_gen_step_tac_opt : holfoot_tactics.gen_step_tac_opt list -> holfoot_tactics.gen_step_tac_opt; 190 val add_inference_groups : (int * holfoot_tactics.var_res_inference_group) list * 191 (int * holfoot_tactics.var_res_inference_group) list * 192 (int * holfoot_tactics.var_res_inference_group) list -> holfoot_tactics.gen_step_tac_opt 193 val no_case_splits : holfoot_tactics.gen_step_tac_opt; 194 val do_case_splits : holfoot_tactics.gen_step_tac_opt; 195 val no_expands : holfoot_tactics.gen_step_tac_opt; 196 val do_expands : holfoot_tactics.gen_step_tac_opt; 197 val full_expands : holfoot_tactics.gen_step_tac_opt; 198 val no_case_split_expands : holfoot_tactics.gen_step_tac_opt; 199 val generate_vcs : holfoot_tactics.gen_step_tac_opt; 200 val dont_generate_vcs : holfoot_tactics.gen_step_tac_opt; 201 val no_asms : holfoot_tactics.gen_step_tac_opt; 202 val use_asms : holfoot_tactics.gen_step_tac_opt; 203 val no_prop_simps : holfoot_tactics.gen_step_tac_opt; 204 val simple_prop_simps : holfoot_tactics.gen_step_tac_opt; 205 val conservative : holfoot_tactics.gen_step_tac_opt; (* not fast *) 206 val careful : holfoot_tactics.gen_step_tac_opt; (* no asms. no case splits, no expands *) 207 val stop_at_cond : holfoot_tactics.gen_step_tac_opt; 208 val stop_at_while : holfoot_tactics.gen_step_tac_opt; 209 val stop_at_abstraction : holfoot_tactics.gen_step_tac_opt; 210 val stop_at_frame_calc : holfoot_tactics.gen_step_tac_opt; 211 val stop_at_hoare_triple : holfoot_tactics.gen_step_tac_opt; 212 val stop_at_block_spec : holfoot_tactics.gen_step_tac_opt; 213 214 val default_holfoot_gst_optL : holfoot_tactics.gen_step_tac_opt list ref; 215 216 val HF_GEN_STEP_CONSEQ_CONV : holfoot_tactics.gen_step_param -> holfoot_tactics.user_rewrite_param -> int option -> int -> Abbrev.thm list -> Abbrev.conv 217 val HF_GEN_STEP_TAC : holfoot_tactics.gen_step_param -> holfoot_tactics.user_rewrite_param -> int option -> int -> Abbrev.tactic 218 val xHF_GEN_STEP_CONSEQ_CONV: holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.conv 219 val xHF_GEN_STEP_TAC : holfoot_tactics.gen_step_tac_opt list -> int option -> int -> Abbrev.tactic 220 221 val xHF_STEP_TAC : holfoot_tactics.gen_step_tac_opt list -> int -> Abbrev.tactic; 222 val xHF_STEP_TAC_n : holfoot_tactics.gen_step_tac_opt list -> int -> int option -> Abbrev.tactic; 223 val xHF_SOLVE_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic; 224 val xHF_CONTINUE_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic; 225 val xHF_SIMPLIFY_TAC : holfoot_tactics.gen_step_tac_opt list -> Abbrev.tactic; 226 227 val HF_STEP_TAC : int -> Abbrev.tactic; 228 val HF_STEP_TAC_n : int -> int option -> Abbrev.tactic; 229 val HF_SOLVE_TAC : Abbrev.tactic; 230 val HF_CONTINUE_TAC : Abbrev.tactic; 231 val HF_SIMPLIFY_TAC : Abbrev.tactic; 232 val HF_VC_SOLVE_TAC : Abbrev.tactic; 233 234 val HF_PURE_VC_TAC : Abbrev.tactic; 235 val HF_ELIM_COMMENTS_TAC : Abbrev.tactic 236 val HF_VC_TAC : Abbrev.tactic; 237 val HF_SPECIFICATION_TAC : Abbrev.tactic 238 val HF_INIT_TAC : Abbrev.tactic 239 val HF_SPECIFICATION_CONSEQ_CONV : ConseqConv.conseq_conv 240 241 242 val holfoot_set_goal : string -> proofManagerLib.proofs 243 val holfoot_set_goal_preprocess : string -> proofManagerLib.proofs 244 val holfoot_set_goal_specs : string -> string list -> proofManagerLib.proofs 245 val holfoot_set_goal_procedures : string -> string list -> proofManagerLib.proofs 246 val holfoot_auto_verify_spec : string -> thm 247 val holfoot_verify_spec : string -> holfoot_tactics.gen_step_tac_opt list -> thm 248 val holfoot_tac_verify_spec : string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> thm 249 val holfoot_interactive_verify_spec : bool -> bool -> string -> (holfoot_tactics.gen_step_tac_opt list) option -> (string * tactic) list -> (thm * bool) 250 val holfoot_prove_remaining : (thm * tactic) -> thm 251 val holfoot_set_remaining_goal : thm -> proofManagerLib.proofs 252 253 val holfoot_prover_extras_1 : thm list ref; 254 val holfoot_prover_extras_2 : thm list ref; 255 val holfoot_varlist_rwts : thm list ref; 256 val update_var_res_param : unit -> unit; 257end 258