1(*************************************************************************** 2 * 3 * jbUtils. sml 4 * 5 * useful conversions, tactics, and ML functions 6 * Jens Brandt 7 * 8 ***************************************************************************) 9 10structure jbUtils :> jbUtils = 11struct 12 13(* interactive mode 14app load ["schneiderUtils"]; 15*) 16 17open HolKernel boolLib Parse bossLib schneiderUtils; 18 19val AND_IMP_RULE = REWRITE_RULE[AND_IMP_INTRO]; 20val IMP_AND_RULE = REWRITE_RULE[GSYM AND_IMP_INTRO]; 21 22(*========================================================================== 23 * tactics 24 *==========================================================================*) 25 26(*-------------------------------------------------------------------------- 27 * REWRITE1_TAC, PROVE1_TAC 28 *--------------------------------------------------------------------------*) 29 30fun ONCE_REWRITE1_TAC(thm1:thm) = ONCE_REWRITE_TAC [thm1]; 31fun REWRITE1_TAC(thm1:thm) = REWRITE_TAC [thm1]; 32fun PROVE1_TAC (thm1:thm) = PROVE_TAC[thm1]; 33 34(*-------------------------------------------------------------------------- 35 * REMAINS_TO_PROVE term -> tactic 36 * 37 * construct new subgoal that solves the current one 38 *--------------------------------------------------------------------------*) 39 40fun REMAINS_TO_PROVE (t:term) = SUBGOAL_THEN t PROVE1_TAC; 41 42(*-------------------------------------------------------------------------- 43 * NEW_GOAL_TAC term -> tactic 44 * 45 * replace current goal by another one (checked by PROVE_TAC) 46 *--------------------------------------------------------------------------*) 47 48fun NEW_GOAL_TAC (t:term) = 49 SUBGOAL_THEN t MATCH_MP_TAC THEN1 PROVE_TAC[]; 50 51(*-------------------------------------------------------------------------- 52 * ASSUME_X_TAC thm -> tactic 53 * 54 * put a new assumption in front of the goal 55 *--------------------------------------------------------------------------*) 56 57fun ASSUME_X_TAC (thm1:thm) = ASSUME_TAC thm1 THEN UNDISCH_HD_TAC; 58 59(*-------------------------------------------------------------------------- 60 * DISJ_LIST_CASES_TAC thm -> tactic 61 * 62 * apply DISJ_CASES_TAC repeatedly for a theorem 63 *--------------------------------------------------------------------------*) 64 65fun DISJ_LIST_CASES_TAC (thm1:thm) (asm_list, goal) = 66let 67 val cases_thm = GEN ``P:bool`` (prove(mk_imp (list_mk_conj (map (fn x => ``^x ==> P:bool``) (strip_disj (concl thm1))), ``P:bool``), PROVE_TAC[thm1])) 68in 69 (MATCH_MP_TAC (SPEC goal cases_thm) THEN REPEAT CONJ_TAC THEN STRIP_TAC) (asm_list, goal) 70end 71 72(*-------------------------------------------------------------------------- 73 * NESTED_ASM_CASES_TAC term list -> tactic 74 * 75 * [a,b,c] -> a \/ ~a /\ (b \/ ~b /\ (c \/ ~c) 76 *--------------------------------------------------------------------------*) 77 78fun NESTED_ASM_CASES_TAC nil = ALL_TAC 79 | NESTED_ASM_CASES_TAC (h::t) = ASM_CASES_TAC (h) THENL [ALL_TAC,(NESTED_ASM_CASES_TAC t)]; 80 81 82(*========================================================================== 83 * ML functions 84 *==========================================================================*) 85 86(*-------------------------------------------------------------------------- 87 * print a message before proving the theorem (for debugging purposes) 88 *--------------------------------------------------------------------------*) 89 90fun store_thm_verbose (s:string, t:term, tac:tactic) = 91 let 92 val _ = print ("Proving " ^ s ^ "...\n") 93 in 94 store_thm(s,t,tac) 95 end; 96 97(*-------------------------------------------------------------------------- 98 * extract_terms_of_type : hol_type -> term -> term list 99 *--------------------------------------------------------------------------*) 100 101fun extract_terms_of_type (typ1:hol_type) (t1:term) = 102 if type_of t1 = typ1 then [t1] 103 else if is_comb t1 then 104 let 105 val (top_rator, top_rand) = dest_comb t1 106 in 107 op_U aconv 108 [extract_terms_of_type typ1 top_rator, 109 extract_terms_of_type typ1 top_rand] 110 end 111 else 112 []; 113 114(*-------------------------------------------------------------------------- 115 * dest_binop_triple : term -> term * term * term 116 *--------------------------------------------------------------------------*) 117 118fun dest_binop_triple tm = 119 let val (Rator,rhs) = Term.dest_comb tm 120 val (opr,lhs) = Term.dest_comb Rator 121 in 122 (opr,lhs,rhs) 123 end; 124 125end; (* of struct *) 126