Update from HH
[hl193./.git] / Jordan / tactics_ext.ml
1 (* This file is in severe need of a rewrite! *)
2
3 unambiguous_interface();;
4 prioritize_real();;
5
6 (* ------------------------------------------------------------------------- *)
7 (* A printer that reverses the assumption list *)
8 (* ------------------------------------------------------------------------- *)
9
10 (*
11
12    Objective version of HOL-light uses (rev asl) in the method print_goal.
13    This means that the numbers printed next to the assumptions
14    are the reverse of the numbering in the list.
15
16    I want it the opposite way.
17    This reverses the numbering on the assumption list,
18    so that the printed numbers match the list order.
19
20    To use, type
21    #install_printer print_rev_goal;;
22    #install_printer print_rev_goalstack;;
23
24    To restore HOL-light defaults, type
25    #install_printer print_goal;;
26    #install_printer print_goalstack;;
27
28 *)
29
30 let (print_rev_goal:goal->unit) =
31   fun (asl,w) ->
32     print_newline();
33     if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
34     print_qterm w; print_newline();;
35
36 let (print_rev_goalstate:int->goalstate->unit) =
37   fun k gs -> let (_,gl,_) = gs in
38               let n = length gl in
39               let s = if n = 0 then "No subgoals" else
40                         (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
41                      ^" ("^(string_of_int n)^" total)" in
42               print_string s; print_newline();
43               if gl = [] then () else
44               do_list (print_rev_goal o C el gl) (rev(0--(k-1)));;
45
46 let (print_rev_goalstack:goalstack->unit) =
47   fun l ->
48     if l = [] then print_string "Empty goalstack"
49     else if tl l = [] then
50       let (_,gl,_ as gs) = hd l in
51       print_rev_goalstate 1 gs
52     else
53       let (_,gl,_ as gs) = hd l
54       and (_,gl0,_) = hd(tl l) in
55       let p = length gl - length gl0 in
56       let p' = if p < 1 then 1 else p + 1 in
57       print_rev_goalstate p' gs;;
58
59 #install_printer print_rev_goal;;
60 #install_printer print_rev_goalstack;;
61
62
63
64
65 (* ------------------------------------------------------------------ *)
66 (* SOME EASY TACTICS *)
67 (* ------------------------------------------------------------------ *)
68
69 let TAUT_TAC t = (MATCH_MP_TAC (TAUT t));;
70
71 let REP_GEN_TAC = REPEAT GEN_TAC;;
72
73 let SUBGOAL_TAC t = SUBGOAL_THEN t MP_TAC;;
74
75 let DISCH_ALL_TAC = REP_GEN_TAC THEN
76   let tac = TAUT_TAC `(b ==> a==> c) ==> (a /\ b ==> c)` in
77   (REPEAT ((REPEAT tac) THEN DISCH_TAC)) THEN LABEL_ALL_TAC;;
78
79 (* ------------------------------------------------------------------ *)
80 (* TACTICS BY NUMBER. These are probably best avoided.
81    NB:
82    The numbering is that in the asm list -- not the printed numbers!  *)
83 (* ------------------------------------------------------------------ *)
84
85 let (UNDISCH_EL_TAC:int -> tactic) =
86  fun i (asl,w) ->
87    try let sthm,asl' = (el i asl),(drop i asl) in
88         let tm = concl (snd (el i asl)) in
89        let thm = snd sthm in
90        null_meta,[asl',mk_imp(tm,w)],
91        fun i [th] -> MP th (INSTANTIATE_ALL i thm)
92    with Failure _ -> failwith "UNDISCH_EL_TAC";;
93
94 (* remove hypotheses by number *)
95 let rec (POPL_TAC:int list ->tactic) =
96   let (POP_TAC:int->tactic) =
97     fun i -> (UNDISCH_EL_TAC i) THEN (TAUT_TAC `B ==> (A==>B)`) in
98   let renumber i =
99     map(fun j -> if j<=i then j else (j-1)) in
100   function [] -> ALL_TAC |
101       (i::b) -> (POP_TAC i) THEN (POPL_TAC (renumber i b));;
102
103 let rec (UNDISCH_LIST:int list -> tactic) =
104   let renumber i =
105     map(fun j -> if j<=i then j else (j-1)) in
106   function [] -> ALL_TAC |
107       (i::b) -> (UNDISCH_EL_TAC i) THEN (UNDISCH_LIST (renumber i b));;
108
109 (* ------------------------------------------------------------------ *)
110 (*   Transformations of Hypothesis List by LABELS                     *)
111 (* ------------------------------------------------------------------ *)
112
113 type goalthm = goal -> thm;;
114
115 let (HYP_INT:int->goalthm) =
116      fun i->
117      fun ((asl,_):goal) ->
118      snd (el i asl);;
119
120 let (HYP:string->goalthm) =
121   fun s (asl,w) ->
122     try assoc s asl
123       with Failure _ -> assoc ("Z-"^s) asl;;
124
125 let (THM:thm->goalthm) =
126      fun thm ->
127      fun (_:goal) -> thm;;
128
129 let (H_RULER: (thm list->thm->thm)->(goalthm list)-> goalthm -> tactic) =
130      fun rule gthl gthm ->
131      fun ((asl,w) as g:goal) ->
132      let thl =  map (fun x-> (x g)) gthl in
133      let th = rule thl  (gthm g) in
134      ASSUME_TAC th g;;
135
136 (* The next few term rules into goal_rules *)
137 (* H_type (x:type) should return an object
138    similar to x but with thms made into goalthms *)
139
140 let (H_RULE_LIST: (thm list->thm->thm)->(goalthm list)-> goalthm -> goalthm) =
141      fun rule gthl gthm g ->
142      let thl =  map (fun x-> (x g)) gthl in
143      rule thl  (gthm g);;
144
145 let H_RULE2 (rule:thm->thm->thm) =
146   fun gthm1 gthm2 -> H_RULE_LIST (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
147
148 let H_RULE (rule:thm->thm) =  fun gthm -> H_RULE_LIST (fun _ th -> rule th) [] gthm;;
149
150 let (H_TTAC : thm_tactic -> goalthm -> tactic ) =
151   fun ttac gthm g -> (ttac (gthm g) g);;
152
153 let H_ASSUME_TAC = H_TTAC ASSUME_TAC;;
154 let INPUT = fun gth -> (H_ASSUME_TAC gth) THEN LABEL_ALL_TAC;;
155
156 let H_VAL2 (rule:thm->thm->thm) =
157   fun gthm1 gthm2 -> H_RULER (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
158
159 let H_CONJ = H_VAL2(CONJ);;
160 let H_MATCH_MP = H_VAL2(MATCH_MP);;
161
162 let H_REWRITE_RULE gthml gth = H_RULER REWRITE_RULE gthml gth;;
163 let H_ONCE_REWRITE_RULE gthml gth = H_RULER ONCE_REWRITE_RULE gthml gth;;
164 let H_SIMP_RULE = H_RULER SIMP_RULE;;
165
166 let H_VAL (rule:thm->thm) = fun gthm -> H_RULER (fun _ th -> rule th) [] gthm;;
167 let H = H_VAL;;
168
169 let H_CONJUNCT1 = H_VAL CONJUNCT1;;
170 let H_CONJUNCT2 = H_VAL CONJUNCT2;;
171 let H_EQT_INTRO = H_VAL EQT_INTRO;;
172 let H_EQT_ELIM  = H_VAL EQT_ELIM;;
173 let H_SPEC = fun t -> H_VAL(SPEC t);;
174 let H_GEN = fun t -> H_VAL(GEN t);;
175 let H_DISJ1 = C (fun t -> H_VAL ((C DISJ1) t));;
176 let H_DISJ2 =  (fun t -> H_VAL (( DISJ2) t));;
177   (* beware! One is inverted here. *)
178 let H_NOT_ELIM = H_VAL (NOT_ELIM);;
179 let H_NOT_INTRO = H_VAL (NOT_INTRO);;
180 let H_EQF_ELIM = H_VAL (EQF_ELIM);;
181 let H_EQF_INTRO = H_VAL (EQF_INTRO);;
182 let (&&&) = H_RULE2 CONJ;;
183
184 let (H_UNDISCH_TAC:goalthm -> tactic) =
185   fun gthm g ->
186     let tm = concl(gthm g) in
187     UNDISCH_TAC tm g;;
188
189
190
191 (* let upgs tac gs = by tac gs;; *)
192
193 let (thm_op:goalthm->goalthm->goalthm) =
194   fun gt1 gt2 g ->
195     if (is_eq (snd (strip_forall (concl (gt1 g)))))
196     then REWRITE_RULE[gt1 g] (gt2 g) else
197     MATCH_MP (gt1 g) (gt2 g);;
198
199 let (COMBO:goalthm list-> goalthm) =
200   fun gthl -> end_itlist thm_op gthl;;
201
202 let INPUT_COMBO = INPUT o COMBO;;
203