Rqe/rqe_tactics_ext.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Labels                                                                *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 let labels_flag = ref false;;
   6
   7 let LABEL_ALL_TAC:tactic =
   8  let mk_label avoid =
   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 =
  14   let rec f_at_i f j =
  15     function [] -> []
  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
  22   fun (asl,w) ->
  23     let aslp = ref asl in
  24     (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
  25     (ALL_TAC (!aslp,w)));;
  26
  27 let e tac = refine(by(VALID
  28    (if !labels_flag then (tac THEN LABEL_ALL_TAC) else tac)));;
  29
  30
  31 (* ---------------------------------------------------------------------- *)
  32 (*  Refinement                                                            *)
  33 (* ---------------------------------------------------------------------- *)
  34
  35
  36 let prove_by_refinement(t,(tacl:tactic list)) =
  37   let gstate = mk_goalstate ([],t) in
  38   let _,sgs,just = rev_itlist
  39     (fun tac gs -> by
  40        (if !labels_flag then (tac THEN LABEL_ALL_TAC) else tac) gs)
  41      tacl gstate in
  42   let th = if sgs = [] then just null_inst []
  43   else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  44   let t' = concl th 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";;
  48
  49 (* ---------------------------------------------------------------------- *)
  50 (*  Term Type Inference Tactics                                                         *)
  51 (* ---------------------------------------------------------------------- *)
  52
  53 let exclude_list = ref
  54 ["=";"FINITE";"COND";"@";"!";"?";"UNION";"DELETE";"CARD";"swap";"IN"];;
  55 (* exclude is needed because polymorphic operators were causing problems *)
  56
  57 let get_var_list tm =
  58   let rec get_var_list tm =
  59     match tm with
  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);;
  65
  66
  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
  72   match new_type with
  73       Tyvar(ns) ->
  74         (match old_type with
  75              Tyvar(os) ->
  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) ->
  79         (match old_type with
  80              Tyvar _ -> []
  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 []
  85                else []);;
  86
  87 let rec auto_theta_list newl oldl =
  88   match newl with
  89       [] -> []
  90     | (h::t) ->
  91         let head_list =
  92           (try
  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);;
  98
  99
 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
 104     inst theta new_tm;;
 105
 106 let rec auto_type_list tm tml =
 107   match tml with
 108       [] -> tm
 109     | (h::t) -> auto_type_list (auto_type tm h) t;;
 110
 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);;
 115
 116 let TYPE_TAC (f:term->tactic) tm =
 117   function (asl,w) as g ->
 118     let typed_term = auto_type_goal tm g in
 119       f typed_term g;;
 120
 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
 124       f typed_terms g;;
 125
 126 (* ---------------------------------------------------------------------- *)
 127 (*  Unfiled                                                               *)
 128 (* ---------------------------------------------------------------------- *)
 129
 130 let CLAIM t =
 131   TYPE_TAC (C SUBGOAL_THEN MP_TAC) t;;
 132
 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";;
 141
 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;;
 145
 146
 147 let rec REPEAT_N_CONV n conv =
 148   if n = 0 then ALL_CONV else conv THENC (REPEAT_N_CONV (n-1) conv);;
 149
 150 let rec REPEAT_N n tac =
 151   if n = 0 then ALL_TAC else tac THEN REPEAT_N (n-1) tac;;
 152
 153 let dest_goal g =
 154   let (asms,conc) = g in (asms:(string * thm) list),(conc:term);;
 155
 156 let DISJ_LCASE g =
 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;
 162       DISJ2_TAC
 163     ]) g;;
 164
 165 let DISJ_RCASE g =
 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;
 171       DISJ1_TAC
 172     ]) g;;
 173
 174 let CASES_ON tm =
 175   let ty,_ = dest_type (type_of tm) in
 176     match ty with
 177         "num" ->
 178           DISJ_CASES_TAC (SPEC tm num_CASES) THENL
 179           [
 180             POP_ASSUM SUBST1_TAC;
 181             POP_ASSUM STRIP_ASSUME_TAC THEN POP_ASSUM SUBST1_TAC
 182           ]
 183       | "bool" ->
 184           DISJ_CASES_TAC (SPEC tm EXCLUDED_MIDDLE)
 185       | _ -> failwith "not a case type";;
 186
 187
 188 let CASES_ON t = TYPE_TAC CASES_ON t;;
 189
 190 let EXISTS_TAC t = TYPE_TAC EXISTS_TAC t;;
 191
 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;;
 195 let USE_IASSUM n =
 196   USE_THEN ("Z-" ^ string_of_int n);;
 197
 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;;
 203
 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;;
 208
 209
 210 let REWRITE_ASSUMS thl = RULE_ASSUM_TAC (REWRITE_RULE thl);;
 211 let ONCE_REWRITE_ASSUMS thl = RULE_ASSUM_TAC (ONCE_REWRITE_RULE thl);;
 212
 213 let REWRITE_ALL_TAC l = REWRITE_ASSUMS l THEN REWRITE_TAC l;;
 214
 215 let rec MATCH_MPL thms =
 216   match thms with
 217       [thm] -> thm
 218     | impl::ant::rest ->
 219         MATCH_MPL ((MATCH_MP impl ant)::rest);;
 220
 221 let rec MATCH_EQ_MPL thms =
 222   match thms with
 223       [thm] -> thm
 224     | impl::ant::rest ->
 225         MATCH_EQ_MPL ((MATCH_EQ_MP impl ant)::rest);;
 226
 227
 228 (*
 229 MATCH_MPL [ASSUME `a ==> b ==> c ==> d`;ASSUME `a:bool`;ASSUME `b:bool`;ASSUME `c:bool`] ;;
 230 *)
 231
 232
 233 let (USE_ASSUM_LIST: string list -> thm_tactic -> tactic) =
 234   fun l ttac ((asl,w) as g) ->
 235     try
 236       let l' = assoc_list l asl in
 237       let l'' = map ttac l' in
 238         (EVERY l'') g
 239     with Failure _ -> failwith "USE_ASSUM_LIST";;
 240
 241 let (KEEP: string list -> tactic) =
 242   fun l (asl,w) ->
 243     try
 244       let asl' = filter (fun x -> mem (fst x) l) asl in
 245         ALL_TAC  (asl',w)
 246     with Failure _ -> failwith "USE_ASSUM_LIST";;
 247
 248
 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));;
 252
 253 let MOVE_TO_FRONT s =
 254   fun (asl,w) ->
 255     let k,asl' = remove (fun x -> fst x = s) asl in
 256       ALL_TAC (k::asl',w);;
 257
 258 let IGNORE x = ALL_TAC;;
 259
 260 let CCONTR_TAC =
 261   MATCH_MP_TAC (TAUT `(~x ==> F) ==> x`) THEN STRIP_TAC;;
 262
 263 let DISCH_ASS = DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);;
 264
 265 let pgoal() =
 266   !current_goalstack;;