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