1 (* This file is in severe need of a rewrite! *)
3 unambiguous_interface();;
6 (* ------------------------------------------------------------------------- *)
7 (* A printer that reverses the assumption list *)
8 (* ------------------------------------------------------------------------- *)
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.
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.
21 #install_printer print_rev_goal;;
22 #install_printer print_rev_goalstack;;
24 To restore HOL-light defaults, type
25 #install_printer print_goal;;
26 #install_printer print_goalstack;;
30 let (print_rev_goal:goal->unit) =
33 if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
34 print_qterm w; print_newline();;
36 let (print_rev_goalstate:int->goalstate->unit) =
37 fun k gs -> let (_,gl,_) = gs 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)));;
46 let (print_rev_goalstack:goalstack->unit) =
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
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;;
59 #install_printer print_rev_goal;;
60 #install_printer print_rev_goalstack;;
65 (* ------------------------------------------------------------------ *)
66 (* SOME EASY TACTICS *)
67 (* ------------------------------------------------------------------ *)
69 let TAUT_TAC t = (MATCH_MP_TAC (TAUT t));;
71 let REP_GEN_TAC = REPEAT GEN_TAC;;
73 let SUBGOAL_TAC t = SUBGOAL_THEN t MP_TAC;;
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;;
79 (* ------------------------------------------------------------------ *)
80 (* TACTICS BY NUMBER. These are probably best avoided.
82 The numbering is that in the asm list -- not the printed numbers! *)
83 (* ------------------------------------------------------------------ *)
85 let (UNDISCH_EL_TAC:int -> tactic) =
87 try let sthm,asl' = (el i asl),(drop i asl) in
88 let tm = concl (snd (el i asl)) 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";;
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
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));;
103 let rec (UNDISCH_LIST:int list -> tactic) =
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));;
109 (* ------------------------------------------------------------------ *)
110 (* Transformations of Hypothesis List by LABELS *)
111 (* ------------------------------------------------------------------ *)
113 type goalthm = goal -> thm;;
115 let (HYP_INT:int->goalthm) =
117 fun ((asl,_):goal) ->
120 let (HYP:string->goalthm) =
123 with Failure _ -> assoc ("Z-"^s) asl;;
125 let (THM:thm->goalthm) =
127 fun (_:goal) -> thm;;
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
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 *)
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
145 let H_RULE2 (rule:thm->thm->thm) =
146 fun gthm1 gthm2 -> H_RULE_LIST (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
148 let H_RULE (rule:thm->thm) = fun gthm -> H_RULE_LIST (fun _ th -> rule th) [] gthm;;
150 let (H_TTAC : thm_tactic -> goalthm -> tactic ) =
151 fun ttac gthm g -> (ttac (gthm g) g);;
153 let H_ASSUME_TAC = H_TTAC ASSUME_TAC;;
154 let INPUT = fun gth -> (H_ASSUME_TAC gth) THEN LABEL_ALL_TAC;;
156 let H_VAL2 (rule:thm->thm->thm) =
157 fun gthm1 gthm2 -> H_RULER (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
159 let H_CONJ = H_VAL2(CONJ);;
160 let H_MATCH_MP = H_VAL2(MATCH_MP);;
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;;
166 let H_VAL (rule:thm->thm) = fun gthm -> H_RULER (fun _ th -> rule th) [] gthm;;
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;;
184 let (H_UNDISCH_TAC:goalthm -> tactic) =
186 let tm = concl(gthm g) in
191 (* let upgs tac gs = by tac gs;; *)
193 let (thm_op:goalthm->goalthm->goalthm) =
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);;
199 let (COMBO:goalthm list-> goalthm) =
200 fun gthl -> end_itlist thm_op gthl;;
202 let INPUT_COMBO = INPUT o COMBO;;