(* ========================================================================= *) (* Isabelle Light *) (* Isabelle/Procedural style additions and other user-friendly shortcuts. *) (* *) (* Petros Papapanagiotou, Jacques Fleuriot *) (* Center of Intelligent Systems and their Applications *) (* University of Edinburgh *) (* 2009-2010 *) (* ========================================================================= *) (* FILE : new_tactics.ml *) (* DESCRIPTION : Various tactics to facilitate procedural-style users. *) (* Mostly inspired by Isabelle's similar tactics. *) (* LAST MODIFIED: October 2012 *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* e_all : tactic -> goalstack *) (* Same as "e" but applies tactic to ALL subgoals. *) (* ------------------------------------------------------------------------- *) let e_all tac = let c = (count_goals()) in let rec f i = ( if (i = 0) then (!current_goalstack) else let _ = e tac in let _ = r 1 in f (i-1) ) in f c;; (* ------------------------------------------------------------------------- *) (* ROTATE_N_TAC: *) (* Rotates assumptions N times. *) (* ------------------------------------------------------------------------- *) (* Pops the entire assumption list doing nothing (K ALL_TAC) then maps *) (* LABEL_TAC to the rotated list of assumptions. The list is reversed so as *) (* to match the external order. The result is applied to (asl,w) so as to *) (* obtain the resulting goalstate as required by the tactic type. *) (* ------------------------------------------------------------------------- *) let (ROTATE_N_TAC :int->tactic) = fun n (asl,w) -> let rotateasm = fun (asl) -> (tl asl)@[hd asl] in (POP_ASSUM_LIST(K ALL_TAC) THEN MAP_EVERY (fun (s,th) -> LABEL_TAC s th) (funpow n rotateasm (rev asl))) (asl,w);; (* ------------------------------------------------------------------------- *) (* ROTATE_TAC: *) (* Rotates assumptions once. *) (* ------------------------------------------------------------------------- *) let (ROTATE_TAC :tactic) = (ROTATE_N_TAC 1);; (* ------------------------------------------------------------------------- *) (* DRULE_N_TAC: *) (* Applies an inference rule to Nth assumption only. *) (* Like drule for HOL Light's inference rules without matching. *) (* ------------------------------------------------------------------------- *) (* Works like RULE_ASSUM_TAC except it numbers the assumption list with *) (* num_list and only applies the rule to the Nth assumption. *) (* ------------------------------------------------------------------------- *) let (DRULE_N_TAC :int->(thm->thm)->tactic) = fun n rule (asl,w) -> (POP_ASSUM_LIST(K ALL_TAC) THEN MAP_EVERY (fun (i,(s,th)) -> LABEL_TAC s (if (i=n) then (rule th) else th)) (num_list(rev asl))) (asl,w);; (* ------------------------------------------------------------------------- *) (* FRULE_N_TAC: *) (* Applies an inference rule to Nth assumption only then adds the result as *) (* a new assumption. *) (* Like frule for HOL Light's inference rules without matching. *) (* ------------------------------------------------------------------------- *) (* Works like DRULE_N_TAC except it leaves the assumption intact and *) (* adds the result as a new assumption. *) (* ------------------------------------------------------------------------- *) let (FRULE_N_TAC :int->(thm->thm)->tactic) = fun n rule (asl,w) -> ( let asmlist = num_list(rev asl) in let (_,asm_n) = try assoc n asmlist with Failure _ -> failwith("FRULE_N_TAC: didn't find assumption "^string_of_int(n)) in ASSUME_TAC (rule asm_n)) (asl,w);; (* ------------------------------------------------------------------------- *) (* FRULE_MN_TAC: *) (* Applies an inference rule (such as MP) to the Mth and Nth assumptions and *) (* adds the result as a new assumption. *) (* ------------------------------------------------------------------------- *) (* Numbers the assumption list, finds the Mth and Nth assumptions, applies *) (* the rule to them and adds the result as a new assumption. *) (* ------------------------------------------------------------------------- *) let (FRULE_MN_TAC :int->int->(thm->thm->thm)->tactic) = fun m n rule (asl,w) -> ( let asmlist = num_list(rev asl) in let (_,asm_m) = try assoc m asmlist with Failure _ -> failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(m)) in let (_,asm_n) = try assoc n asmlist with Failure _ -> failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(n)) in ASSUME_TAC (rule asm_m asm_n)) (asl,w);; (* ------------------------------------------------------------------------- *) (* ----------------------- SIMP TACTICS START HERE!! ----------------------- *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* GENERAL_ASM_TAC: (thm list -> thm -> thm) -> thm list -> tactic *) (* General function that uses a rewrite rule to rewrite the assumptions. *) (* Each assumption is rewritten using the rest of the assumptions and the *) (* given list of theorems. *) (* ------------------------------------------------------------------------- *) (* A filter is applied to ensure that the assumption is not used to rewrite *) (* itself. *) (* ------------------------------------------------------------------------- *) let GENERAL_ASM_TAC = fun rule thl (asl,w) -> let asm = map snd asl in (POP_ASSUM_LIST(K ALL_TAC) THEN MAP_EVERY (fun (s,th) -> LABEL_TAC s (rule ((filter (fun x -> not (th = x)) asm) @ thl) th) ) (rev asl)) (asl,w);; (* ------------------------------------------------------------------------- *) (* Using the above GENERAL_ASSUM_TAC, we define 4 tactics to rewrite *) (* assumptions based on the 4 rewrite rules available in HOL Light. *) (* ------------------------------------------------------------------------- *) let REWRITE_ASM_TAC,ONCE_REWRITE_ASM_TAC,PURE_REWRITE_ASM_TAC, PURE_ONCE_REWRITE_ASM_TAC = GENERAL_ASM_TAC REWRITE_RULE, GENERAL_ASM_TAC ONCE_REWRITE_RULE, GENERAL_ASM_TAC PURE_REWRITE_RULE, GENERAL_ASM_TAC PURE_ONCE_REWRITE_RULE;; (* ------------------------------------------------------------------------- *) (* And for simplification. *) (* ------------------------------------------------------------------------- *) let SIMP_ASM_TAC,ONCE_SIMP_ASM_TAC,PURE_SIMP_ASM_TAC = GENERAL_ASM_TAC SIMP_RULE, GENERAL_ASM_TAC ONCE_SIMP_RULE, GENERAL_ASM_TAC PURE_SIMP_RULE;; (* ------------------------------------------------------------------------- *) (* FULL_REWRITE_TAC : thm list -> tactic *) (* simp : thm list -> tactic *) (* Similar to Isabelle's simp. Rewrites assumptions then rewrites goal *) (* using the assumptions. *) (* ------------------------------------------------------------------------- *) let FULL_REWRITE_TAC thl = REWRITE_ASM_TAC thl THEN ASM_SIMP_TAC thl;; let simp = FULL_REWRITE_TAC;; (* ------------------------------------------------------------------------- *) (* FULL_SIMP_TAC : thm list -> tactic *) (* Hybrid simplifier. Uses HOL Light's SIMP_TAC then FULL_REWRITE_TAC. *) (* ------------------------------------------------------------------------- *) let FULL_SIMP_TAC thl = SIMP_TAC thl THEN REWRITE_ASM_TAC thl THEN ASM_REWRITE_TAC thl;; (* ------------------------------------------------------------------------- *) (* assumption (tactic): *) (* Shortcut to match an assumption to the goal as Isabelle's "assumption". *) (* ------------------------------------------------------------------------- *) let assumption = FIRST_ASSUM MATCH_ACCEPT_TAC;; (* ------------------------------------------------------------------------- *) (* ALL_UNIFY_ACCEPT_TAC (term list -> thm -> tactic): *) (* Altered UNIFY_ACCEPT_TAC. Uses INSTANTIATE_ALL instead of INSTANTIATE. *) (* ------------------------------------------------------------------------- *) (* This allows for some valid instantiations that weren't otherwise allowed. *) (* eg After using allE, the `a` metavariable can't be instantiated otherwise.*) (* ------------------------------------------------------------------------- *) let ALL_UNIFY_ACCEPT_TAC mvs th (asl,w) = let insts = term_unify mvs (concl th) w in ([],insts),[], let th' = INSTANTIATE_ALL insts th in fun i [] -> INSTANTIATE_ALL i th';; (* ------------------------------------------------------------------------- *) (* meta_assumption (term list -> tactic): *) (* Shortcut to match an assumption to the goal as Isabelle's "assumption". *) (* This version also tries unification by instantiation of meta-variables *) (* which, unfortunately, need to be given manually in a list. *) (* ------------------------------------------------------------------------- *) (* Invalid instantiations may be produced. *) (* eg g `!x:num. (?a:num. R a x) ==> (?y. R y x)`;; *) (* e GEN_TAC;; *) (* e (rule impI);; *) (* e (rule exI);; *) (* e (FIRST_X_ASSUM (X_CHOOSE_TAC `b:num`));; *) (* e (meta_assumption [`a:num`]);; *) (* This succeeds but top_thm() is unable to reconstruct the theorem. *) (* ------------------------------------------------------------------------- *) let meta_assumption mvs = (FIRST_ASSUM MATCH_ACCEPT_TAC) ORELSE (FIRST_ASSUM (ALL_UNIFY_ACCEPT_TAC mvs));; (* ------------------------------------------------------------------------- *) (* Shortcut for interactive proofs so that you don't have to enumerate *) (* metavariables. *) (* ------------------------------------------------------------------------- *) let ema () = (e o meta_assumption o top_metas o p) () ;; (* ------------------------------------------------------------------------- *) (* X_MATCH_CHOOSE_TAC : (term -> tactic) *) (* Version of X_CHOOSE_TAC with type matching. *) (* ------------------------------------------------------------------------- *) (* If the variable given as an argument has a vartype then its type is *) (* instantiated to the type of the existentially quantified variable. *) (* Usefull so that the user need not specify the type for his variable. *) (* It is still acceptable if the user does specify it. *) (* ------------------------------------------------------------------------- *) let (X_MATCH_CHOOSE_TAC: term -> thm_tactic) = fun x' xth -> try let xtm = concl xth in let x,bod = dest_exists xtm in let x'type = type_of x' in let x'' = if (is_vartype x'type) then inst (type_match x'type (type_of x) []) x' else x' in let pat = vsubst[x'',x] bod in let xth' = ASSUME pat in fun (asl,w) -> let avoids = itlist (union o frees o concl o snd) asl (union (frees w) (thm_frees xth)) in if mem x' avoids then failwith "X_CHOOSE_TAC" else null_meta,[("",xth')::asl,w], fun i [th] -> CHOOSE(x'',INSTANTIATE_ALL i xth) th with Failure _ -> failwith "X_CHOOSE_TAC";; (* ------------------------------------------------------------------------- *) (* exE : (term -> tactic) *) (* Existential elimination tactic (since we are unable to accommodate *) (* erule exE with the current meta_rule system because of lack of meta-level *) (* quantification). *) (* ------------------------------------------------------------------------- *) let exE = FIRST_X_ASSUM o X_MATCH_CHOOSE_TAC;; (* ------------------------------------------------------------------------- *) (* allI : (term -> tactic) *) (* Universal introduction tactic (since we are unable to accommodate *) (* rule allI with the current meta_rule system because of lack of meta-level *) (* quantification). *) (* ------------------------------------------------------------------------- *) (* (+) We can use X_GEN_TAC to allow the user to give his own term, but *) (* this is rarely useful in procedural style proofs. *) (* ------------------------------------------------------------------------- *) let allI = GEN_TAC;; (* ------------------------------------------------------------------------- *) (* qed : (unit -> thm) *) (* Reconstructs the theorem at the end of an interactive proof. *) (* May fail if an incorrect metavariable instantiation has occured during the*) (* proof. *) (* ------------------------------------------------------------------------- *) (* (+) There are plans to upgrade this for better accommodation of proofs *) (* containing meta-level implication (see meta_rules.ml and gmm). *) (* ------------------------------------------------------------------------- *) let qed = top_thm;; (* ------------------------------------------------------------------------- *) (* ASM_STRUCT_CASES_TAC : (thm_tactic) *) (* Replacement/fix of STRUCT_CASES_TAC where each case is added as an *) (* assumption like ASM_CASES_TAC does for booleans. *) (* ------------------------------------------------------------------------- *) let ASM_STRUCT_CASES_TAC = REPEAT_TCL STRIP_THM_THEN ASSUME_TAC;; (* ------------------------------------------------------------------------- *) (* case_tac : (term -> tactic) *) (* Isabelle's case_tac for splitting cases. *) (* ------------------------------------------------------------------------- *) let (case_tac:term->tactic) = fun tm ((_,w) as g) -> let trymatch = fun tm1 tm2 -> try ( let inst = term_match (gl_frees g) tm1 tm2 in if (is_var tm1) then match inst with [],[],_ -> true | _ -> false else true ) with Failure _ -> false in let tm' = try (find_term (trymatch tm) w) with Failure _ -> tm in let ty = (fst o dest_type o type_of) tm' in let thm = try (cases ty) with Failure _ -> failwith ("case_tac: Failed to find cases theorem for type \"" ^ ty ^ "\".") in ASM_STRUCT_CASES_TAC (ISPEC tm' thm) g;; (* ------------------------------------------------------------------------- *) (* gen_case_tac : tactic *) (* Case split on the leading universal quantifier of the goal. *) (* ------------------------------------------------------------------------- *) let (gen_case_tac:tactic) = fun ((_,w) as g) -> case_tac ((fst o dest_forall) w) g;; (* ------------------------------------------------------------------------- *) (* subgoal_tac : (term -> tactic) *) (* Introduces a new subgoal which gets added as an assumption. *) (* Isabelle's subgoal_tac. *) (* ------------------------------------------------------------------------- *) let subgoal_tac = fun tm -> SUBGOAL_THEN tm ASSUME_TAC;; (* ------------------------------------------------------------------------- *) (* meson : (thm list -> tactic) *) (* Lower-case shortcut for ASM_MESON_TAC *) (* ------------------------------------------------------------------------- *) let meson = ASM_MESON_TAC;;