1 (* ---------------------------------------------------------------------- *)
3 (* ---------------------------------------------------------------------- *)
5 let labels_flag = ref false;;
7 let LABEL_ALL_TAC:tactic =
9 let rec mk_one_label i avoid =
10 let label = "Z-"^(string_of_int i) in
11 if not(mem label avoid) then label else mk_one_label (i+1) avoid in
12 mk_one_label 0 avoid in
13 let update_label i asl =
16 | a::b -> if (j=0) then (f a)::b else a::(f_at_i f (j-1) b) in
17 let avoid = map fst asl in
18 let current = el i avoid in
19 let new_label = mk_label avoid in
20 if (String.length current > 0) then asl else
21 f_at_i (fun (_,y) -> (new_label,y) ) i asl in
24 (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
25 (ALL_TAC (!aslp,w)));;
27 let e tac = refine(by(VALID
28 (if !labels_flag then (tac THEN LABEL_ALL_TAC) else tac)));;
31 (* ---------------------------------------------------------------------- *)
33 (* ---------------------------------------------------------------------- *)
36 let prove_by_refinement(t,(tacl:tactic list)) =
37 let gstate = mk_goalstate ([],t) in
38 let _,sgs,just = rev_itlist
40 (if !labels_flag then (tac THEN LABEL_ALL_TAC) else tac) gs)
42 let th = if sgs = [] then just null_inst []
43 else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
45 if t' = t then th else
46 try EQ_MP (ALPHA t' t) th
47 with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
49 (* ---------------------------------------------------------------------- *)
50 (* Term Type Inference Tactics *)
51 (* ---------------------------------------------------------------------- *)
53 let exclude_list = ref
54 ["=";"FINITE";"COND";"@";"!";"?";"UNION";"DELETE";"CARD";"swap";"IN"];;
55 (* exclude is needed because polymorphic operators were causing problems *)
58 let rec get_var_list tm =
60 Var(name,ty) -> [name,ty]
61 | Const(name,ty) -> [name,ty]
62 | Abs(bv,bod) -> union (get_var_list bv) (get_var_list bod)
63 | Comb(s,t) -> union (get_var_list s) (get_var_list t) in
64 filter (fun x -> not (mem (fst x) !exclude_list)) (get_var_list tm);;
67 let rec auto_theta new_type old_type =
68 let tyvar_prefix = "?" in
69 let is_generated ty_name =
70 let first_char = hd(explode ty_name) in
71 if first_char = tyvar_prefix then true else false in
76 if is_generated ns then [old_type,new_type] else []
77 | Tyapp (old_name,old_list) -> [old_type,new_type])
78 | Tyapp(new_ty_op,new_ty_list) ->
81 | Tyapp (old_ty_op,old_ty_list) ->
82 if new_ty_op = old_ty_op then
83 itlist2 (fun newt oldt b -> union (auto_theta newt oldt) b)
84 new_ty_list old_ty_list []
87 let rec auto_theta_list newl oldl =
93 let new_name,new_type = h in
94 let old_type = assoc new_name oldl in
95 (auto_theta new_type old_type)
96 with Failure _ -> []) in
97 union head_list (auto_theta_list t oldl);;
100 let auto_type new_tm old_tm =
101 let old_list = get_var_list old_tm in
102 let new_list = get_var_list new_tm in
103 let theta = auto_theta_list new_list old_list in
106 let rec auto_type_list tm tml =
109 | (h::t) -> auto_type_list (auto_type tm h) t;;
111 let auto_type_goal tm (asl,w) =
112 let thm_list = snd(unzip asl) in
113 let term_list = map (fun x -> snd (dest_thm x)) thm_list in
114 auto_type_list tm ([w] @ term_list);;
116 let TYPE_TAC (f:term->tactic) tm =
117 function (asl,w) as g ->
118 let typed_term = auto_type_goal tm g in
121 let TYPE_TACL (f:term list -> tactic) tml =
122 function (asl,w) as g ->
123 let typed_terms = map (C auto_type_goal g) tml in
126 (* ---------------------------------------------------------------------- *)
128 (* ---------------------------------------------------------------------- *)
131 TYPE_TAC (C SUBGOAL_THEN MP_TAC) t;;
133 let lem = TAUT `(a = b) <=> (a ==> b) /\ (b ==> a)`;;
134 let MATCH_EQ_MP t1 t2 =
135 try EQ_MP t1 t2 with Failure _ ->
136 let k1 = (SPEC_ALL (PURE_REWRITE_RULE[lem] t1)) in
137 let left,right = CONJUNCT1 k1,CONJUNCT2 k1 in
138 try MATCH_MP left t2 with Failure _ ->
139 try MATCH_MP right t2 with Failure _ ->
140 failwith "MATCH_EQ_MP";;
142 let MATCH_EQ_MP_TAC thm =
143 let t1,t2 = EQ_IMP_RULE (SPEC_ALL thm) in
144 MATCH_MP_TAC t1 ORELSE MATCH_MP_TAC t2;;
147 let rec REPEAT_N_CONV n conv =
148 if n = 0 then ALL_CONV else conv THENC (REPEAT_N_CONV (n-1) conv);;
150 let rec REPEAT_N n tac =
151 if n = 0 then ALL_TAC else tac THEN REPEAT_N (n-1) tac;;
154 let (asms,conc) = g in (asms:(string * thm) list),(conc:term);;
157 let _,c = dest_goal g in
158 let l,r = dest_disj c in
159 let thm = ISPEC l EXCLUDED_MIDDLE in
160 (DISJ_CASES_TAC thm THENL [
161 DISJ1_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
166 let _,c = dest_goal g in
167 let l,r = dest_disj c in
168 let thm = ISPEC r EXCLUDED_MIDDLE in
169 (DISJ_CASES_TAC thm THENL [
170 DISJ2_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
175 let ty,_ = dest_type (type_of tm) in
178 DISJ_CASES_TAC (SPEC tm num_CASES) THENL
180 POP_ASSUM SUBST1_TAC;
181 POP_ASSUM STRIP_ASSUME_TAC THEN POP_ASSUM SUBST1_TAC
184 DISJ_CASES_TAC (SPEC tm EXCLUDED_MIDDLE)
185 | _ -> failwith "not a case type";;
188 let CASES_ON t = TYPE_TAC CASES_ON t;;
190 let EXISTS_TAC t = TYPE_TAC EXISTS_TAC t;;
192 let REWRITE_ASSUMS thl = RULE_ASSUM_TAC (REWRITE_RULE thl);;
193 let ONCE_REWRITE_ASSUMS thl = RULE_ASSUM_TAC (ONCE_REWRITE_RULE thl);;
194 let REWRITE_ALL thl = REWRITE_ASSUMS thl THEN REWRITE_TAC thl;;
196 USE_THEN ("Z-" ^ string_of_int n);;
198 let PROVE_ASSUM_ANTECEDENT_TAC n =
199 fun ((asl,w) as g) ->
200 let assum = assoc ("Z-" ^ string_of_int n) asl in
201 let ant,_ = dest_imp (concl assum) in
202 SUBGOAL_THEN ant (fun x -> (USE_IASSUM n (fun y-> ASSUME_TAC (MATCH_MP y x)))) g;;
204 let FALSE_ANTECEDENT_TAC =
205 fun ((asl,w) as g) ->
206 let l,r = dest_imp w in
207 (SUBGOAL_THEN (mk_neg l) (fun x -> REWRITE_TAC[x])) g;;
210 let REWRITE_ASSUMS thl = RULE_ASSUM_TAC (REWRITE_RULE thl);;
211 let ONCE_REWRITE_ASSUMS thl = RULE_ASSUM_TAC (ONCE_REWRITE_RULE thl);;
213 let REWRITE_ALL_TAC l = REWRITE_ASSUMS l THEN REWRITE_TAC l;;
215 let rec MATCH_MPL thms =
219 MATCH_MPL ((MATCH_MP impl ant)::rest);;
221 let rec MATCH_EQ_MPL thms =
225 MATCH_EQ_MPL ((MATCH_EQ_MP impl ant)::rest);;
229 MATCH_MPL [ASSUME `a ==> b ==> c ==> d`;ASSUME `a:bool`;ASSUME `b:bool`;ASSUME `c:bool`] ;;
233 let (USE_ASSUM_LIST: string list -> thm_tactic -> tactic) =
234 fun l ttac ((asl,w) as g) ->
236 let l' = assoc_list l asl in
237 let l'' = map ttac l' in
239 with Failure _ -> failwith "USE_ASSUM_LIST";;
241 let (KEEP: string list -> tactic) =
244 let asl' = filter (fun x -> mem (fst x) l) asl in
246 with Failure _ -> failwith "USE_ASSUM_LIST";;
249 let PROVE_THM_ANTECEDENT_TAC thm =
250 let ant,cons = dest_imp (concl thm) in
251 SUBGOAL_THEN ant (fun x -> MP_TAC (MATCH_MP thm x));;
253 let MOVE_TO_FRONT s =
255 let k,asl' = remove (fun x -> fst x = s) asl in
256 ALL_TAC (k::asl',w);;
258 let IGNORE x = ALL_TAC;;
261 MATCH_MP_TAC (TAUT `(~x ==> F) ==> x`) THEN STRIP_TAC;;
263 let DISCH_ASS = DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);;