1 2(* miscellaneous useful stuff that doesn't fit in anywhere else *) 3structure commonTools = 4struct 5 6local 7 8open Globals HolKernel Parse Feedback 9 10open bossLib pairTheory pred_setTheory pred_setLib stringLib simpLib pairSyntax pairLib PrimitiveBddRules DerivedBddRules Binarymap PairRules pairTools boolSyntax Drule Tactical Conv Rewrite Tactic boolTheory stringTheory boolSimps pureSimps numLib sumSyntax sumTheory listTheory 11open stringBinTree lazyTools setLemmasTheory 12 13val dpfx = "comt_" 14 15in 16 17fun pair_map f (x,y) = (f x,f y) 18 19(*********** math **************) 20 21fun ilog2 n = if n=1 then 1 else Real.floor(((Math.ln (Real.fromInt(n)))/(Math.ln 2.0))+1.0); (* NOTE:this is NOT log_2 *) 22 23fun log2 n = Math.ln n / Math.ln 2.0 24 25(* taken from Mike's HOL history paper. Attributed to C. Strachey. *) 26fun cartprod L = List.foldr (fn (k,z) => List.foldr (fn (x,y) => List.foldr (fn (p,q) => (x::p)::q) y z) [] k) [[]] L 27 28fun fromMLnum n = numSyntax.mk_numeral(Arbnum.fromInt n); 29 30(************ HOL **************) 31 32fun tsimps ty = let val {convs,rewrs} = TypeBase.simpls_of ty in rewrs end; 33 34val get_ss_rewrs = simpLib.frag_rewrites 35 36(* make abbrev def: make definition where the lhs is just a constant name and rhs is closed term with no free_vars *) 37fun mk_adf nm rhs = 38let val x = mk_var("x",type_of rhs ) 39in new_specification(nm^"_def",[nm],EXISTS (mk_exists(x,mk_eq(x,rhs))(*``?x. x = ^rhs``*),rhs) (REFL rhs)) end 40 41fun LIST_ACCEPT_TAC l (asl,w) = 42 let val th = hd(List.filter (aconv w o concl) l) 43 in ACCEPT_TAC th (asl,w) end 44 45(* simpset that is just beta reduction *) 46val BETA_ss = SSFRAG 47 {name = SOME "BETA_ss", 48 convs=[{name="BETA_CONV (beta reduction)", 49 trace=2, 50 key=SOME ([],(--`(\x:'a. y:'b) z`--)), 51 conv=K (K BETA_CONV)}], 52 rewrs=[], congs = [], filter = NONE, ac = [], dprocs = []}; 53 54val REDUCE_ss = SSFRAG 55 {name = SOME "REDUCE_ss", 56 convs=[{name="REDUCE_CONV (num reduction)", 57 trace=2, 58 key=SOME ([],(--`(x:num)-1`--)), 59 conv=K (K REDUCE_CONV)}], 60 rewrs=[], congs = [], filter = NONE, ac = [], dprocs = []}; 61 62val EL_ss = SSFRAG 63 {name = SOME "EL_ss", 64 convs=[{name="num_CONV (num to suc conversion)", 65 trace=2, 66 key=SOME ([],(--`EL (x:num)`--)), 67 conv=K (K (RAND_CONV numLib.num_CONV))}], 68 rewrs=[EL,HD,TL], congs = [], filter = NONE, ac = [], dprocs = []}; 69 70fun UNCHANGED_CONV conv tm = conv tm handle UNCHANGED => REFL tm 71 72fun NCONV n conv = if n=0 then ALL_CONV else conv THENC NCONV (n-1) conv 73 74(* given p IN {s_1,...,s_n}, proves = to \/_i p = s_i *) 75fun IN_FIN_CONV t = PURE_REWRITE_CONV [NOT_IN_EMPTY,IN_INSERT,GEN_ALL (List.nth(CONJUNCTS (SPEC_ALL OR_CLAUSES),3))] t 76 77(************ strings ************) 78 79(* replace all spaces in s with underscores *) 80fun despace s = implode (List.map (fn c => if Char.compare(c,#" ")=EQUAL then #"_" else c) (explode s)) 81 82fun prm s = s^"'" 83 84(*********** lists **************) 85 86(* given a list [a,b,c,d,...], return the list [(a,b),(b,c),(c,d)...]*) 87fun threadlist (h1::h2::t) = (h1,h2)::(threadlist (h2::t)) 88| threadlist [h] = [] 89| threadlist [] = [] 90 91(* given a list [a,b,c...] and a list [1,2,3...], return [a,1,b,2,...] *) 92(* both lists should be same length, otherwise exception *) 93fun interleave (h1::t1) (h2::t2) = h1::h2::(interleave t1 t2) 94| interleave [] [] = [] 95| interleave l1 l2 = failwith ("Match exception in commonTools.interleave") 96 97(* just discovered this is already present as Lib.split_after (though not sure if that behaves exactly like this) *) 98fun split_list [] n = ([],[]) 99 | split_list (h::t) n = let val (M,N)=split_list (t) (n-1) 100 in if (n>0) then (h::M,N) else (M,h::N) end 101 102fun listmax l = List.foldl (fn (i,m) => if m<i then i else m) (Option.valOf Int.minInt) l 103 104fun listmap cf (h::t) = Binarymap.insert(listmap cf t, (fst h), (snd h)) 105| listmap cf [] = Binarymap.mkDict cf; 106 107fun list2set cf (h::t) = Binaryset.add(list2set cf t,h) 108| list2set cf [] = Binaryset.empty cf; 109 110fun list2imap l = listmap Int.compare l 111 112fun list2map l = listmap String.compare l 113 114fun listkeyfind (h::t) k cf = if (cf(k,fst h)=EQUAL) then snd h else listkeyfind t k cf 115| listkeyfind [] _ _ = Raise NotFound 116 117(* chop up a list into lists of length n, though the last list will just take up the slack *) 118fun multi_part n l = if (List.length l) <= n then [l] 119 else let val (bf,af) = split_list l n 120 in bf::(multi_part n af) end 121 122(* remove duplicates from list l, under comparison function f *) 123fun undup f l = Binaryset.listItems(Binaryset.addList(Binaryset.empty f,l)) 124 125(* this is better than listSyntax.mk_list because it figures out the type by itself*) 126fun fMl ty (h::t) = listSyntax.mk_cons(h,fMl ty t) 127| fMl ty [] = listSyntax.mk_nil ty 128 129fun fromMLlist (h::t) = fMl (type_of h) (h::t) 130| fromMLlist [] = listSyntax.mk_nil alpha 131 132(*********** terms **************) 133 134fun mk_subst red res = (map2 (curry op|->) red res) 135 136fun dest_subst {redex,residue} = (redex,residue) 137 138val mk_var = Term.mk_var; 139 140val land = rand o rator 141 142fun setify cf l = HOLset.listItems(HOLset.addList(HOLset.empty cf,l)) 143 144fun mk_bool_var v = mk_var(v,bool); 145 146fun mk_primed_bool_var v = mk_bool_var (v^"'"); 147 148fun is_bool_var v = is_var v andalso (Type.compare(type_of v,bool)=EQUAL) 149 150fun is_T tm = Term.compare(tm,T)=EQUAL 151 152fun is_F tm = Term.compare(tm,F)=EQUAL 153 154fun is_prop_tm tm = 155 if is_neg tm 156 then is_prop_tm (rand tm) 157 else 158 if is_conj tm orelse is_imp tm orelse is_disj tm orelse is_cond tm orelse is_eq tm 159 then is_prop_tm (land tm) andalso is_prop_tm (rand tm) 160 else 161 if (is_forall tm) 162 then let val (v,t) = dest_forall tm 163 in is_bool_var v andalso is_prop_tm t end 164 else 165 if is_exists tm 166 then let val (v,t) = dest_exists tm 167 in is_bool_var v andalso is_prop_tm t end 168 else is_T tm orelse is_F tm orelse is_bool_var tm 169 170fun term_to_string2 t = with_flag (show_types,false) term_to_string t; 171 172fun prime v = mk_var((term_to_string2 v)^"'",type_of v) 173 174fun is_prime v = (Char.compare(List.last(explode(term_to_string2 v)),#"'")=EQUAL) 175 176fun unprime v = if is_prime v then mk_var(implode(butlast(explode(term_to_string2 v))),type_of v) else v 177 178fun list_mk_disj2 [] = F 179 | list_mk_disj2 l = list_mk_disj l 180 181fun list_mk_conj2 [] = T 182 | list_mk_conj2 l = list_mk_conj l 183 184(* break apart all top-level conjunctions *) 185fun list_dest_conj t = if (is_conj t) then (if (is_conj(fst (dest_conj t))) then list_dest_conj(fst (dest_conj t)) 186 else [fst (dest_conj t)])@ 187 (if (is_conj(snd (dest_conj t))) then list_dest_conj(snd (dest_conj t)) 188 else [snd (dest_conj t)]) 189 else [t]; 190 191(* assume t=(c,f1,f2) is a nested conditional, return a list of all the conditions *) 192fun depth_dest_cond_aux (c,f1,f2) = 193 let val l1 = if (is_cond f1) then depth_dest_cond_aux (dest_cond f1) else [] 194 val l2 = if (is_cond f2) then depth_dest_cond_aux (dest_cond f2) else [] 195 in c::(l1@l2) end 196 197fun depth_dest_cond t = if is_cond t then depth_dest_cond_aux (dest_cond t) else [t] 198 199fun list_dest_cond_aux (c,f1,f2) = if is_cond f2 then (c,f1)::(list_dest_cond_aux (dest_cond f2)) else [(c,f1)] 200 201(* destroy linear nested conditional, returning (test,true branch) pairs (the last false branch is dropped) *) 202fun list_dest_cond t = if is_cond t then list_dest_cond_aux (dest_cond t) else [] 203 204fun gen_dest_cond_aux (c,f1,f2) = 205 let val l1 = if (is_cond f1) then gen_dest_cond_aux (dest_cond f1) else [([],f1)] 206 val l2 = if (is_cond f2) then gen_dest_cond_aux (dest_cond f2) else [([],f2)] 207 in (List.map (fn (l,v) => (c::l,v)) l1)@(List.map (fn (l,v) => (l,v)) l2) end 208 209(* destroy general conditional, returning (list of tests,value) pairs *) 210fun gen_dest_cond t = if is_cond t then gen_dest_cond_aux (dest_cond t) else [] 211 212(* conversion for pushing in implications in an implication chain *) 213 214(* push outermost implication in one step *) 215(* assume tm is of the form t0 ==> .... ==> tn, where n is at least 2 *) 216 217fun PUSH_IMP_CONV tm = PURE_ONCE_REWRITE_CONV [PUSH_IMP_THM] tm 218 219fun PUSHN_IMP_CONV n = if n=0 then REFL else PUSH_IMP_CONV THENC RAND_CONV (PUSHN_IMP_CONV (n-1)) 220 221(* my own version of ELIM_TULPED_QUANT_CONV *) 222 223(* vacuous quantification. Will fail if v is free in tm *) 224fun MK_VACUOUS_QUANT_CONV mk_quant v tm = 225 let val t2 = mk_quant(v,tm) 226 in prove(mk_eq(tm,t2),REWRITE_TAC []) end (* FIXME: stop being lazy and make this quicker *) 227 228(* push outermost quantifier inwards n times through same quants. Will fail if there aren't enough quants or if they are not the same *) 229fun PUSH_QUANT_CONV swap_quant_conv n = 230 if n=0 then REFL else swap_quant_conv THENC QUANT_CONV (PUSH_QUANT_CONV swap_quant_conv (n-1)) 231 232(* my own version of pairTools.ELIM_TUPLED_QUANT_CONV that fixes the "impreciseness" (see comments in pairTools) *) 233(* also fixes a crash if the target term is of the form ``\quant <varstruct> othervars. body``. Now works if othervars are present *) 234(* also leaves non-paired quants unchanged rather than crashing *) 235local 236 val is_uncurry_tm = same_const pairSyntax.uncurry_tm 237 val is_universal = same_const boolSyntax.universal 238 val is_existential = same_const boolSyntax.existential 239 val CONV = fn n => EVERY_CONV (List.tabulate(n,fn n => Ho_Rewrite.PURE_ONCE_REWRITE_CONV [pairTheory.ELIM_UNCURRY])) THENC 240 DEPTH_CONV BETA_CONV THENC 241 Ho_Rewrite.PURE_REWRITE_CONV [pairTheory.ELIM_PEXISTS,pairTheory.ELIM_PFORALL] 242 243 fun dest_tupled_quant tm = 244 case total dest_comb tm 245 of NONE => NONE 246 | SOME(f,x) => 247 if is_comb x andalso is_uncurry_tm (rator x) 248 then if is_existential f then SOME (strip_exists, list_mk_exists, pairSyntax.dest_pexists, 249 fn v => fn n => CONV_RULE (RHS_CONV ((MK_VACUOUS_QUANT_CONV mk_exists v) 250 THENC (PUSH_QUANT_CONV SWAP_EXISTS_CONV n)))) else 251 if is_universal f then SOME (strip_forall, list_mk_forall, pairSyntax.dest_pforall, 252 fn v => fn n => CONV_RULE (RHS_CONV ((MK_VACUOUS_QUANT_CONV mk_forall v) 253 THENC (PUSH_QUANT_CONV SWAP_VARS_CONV n)))) 254 else NONE 255 else NONE 256in 257 258fun ELIM_TUPLED_QUANT_CONV tm = 259 if not (is_pair (fst ((if is_pforall tm then dest_pforall else dest_pexists) tm))) then REFL tm 260 else case dest_tupled_quant tm 261 of NONE => raise Fail "TUPLED_QUANT_CONV" 262 | SOME (strip_quant, list_mk_quant, dest_pquant,thm_rule) => 263 let val (tmq,tmbody) = dest_pquant tm 264 val V = strip_pair tmq 265 val thm = CONV ((List.length V)-1) tm 266 val bodyvarset = Binaryset.addList(Binaryset.empty Term.compare, free_vars tmbody) 267 val Vset = Binaryset.addList(Binaryset.empty Term.compare, V) 268 val rside = rhs(concl thm) 269 val ((W,W'),body) = ((fn l => split_list l (List.length V)) ## I) (strip_quant rside) 270 in TRANS thm (ALPHA rside (list_mk_quant(V@W', subst(map2 (curry op|->) W V) body))) 271 end 272end 273 274fun lzELIM_TUPLED_QUANT_CONV tm = 275 let val ia = is_pforall tm 276 val (bv,bod) = if ia then dest_pforall tm else dest_pexists tm 277 in mk_lthm (fn _ => (mk_eq(tm,if ia then list_mk_forall(spine_pair bv,bod) else list_mk_exists(spine_pair bv,bod)), 278 (fn _ => ELIM_TUPLED_QUANT_CONV tm))) 279 (fn _ => ELIM_TUPLED_QUANT_CONV tm) end 280 281(*********** sums **************) 282 283fun mk_sum_component_aux n i s = 284 if (i=0) then sumSyntax.mk_inl(s,mk_vartype("'a"^(int_to_string i))) 285 else if (i=1 andalso n=2) then sumSyntax.mk_inr(s,mk_vartype("'a"^(int_to_string i))) 286 else sumSyntax.mk_inr(mk_sum_component_aux (n-1) (i-1) s,mk_vartype("'a"^(int_to_string i))) 287 288(* returns s tagged with INL's and INR's so that its type is the i'th component of the sum ty_0+ty_1+...+ty_(n-1) *) 289fun mk_sum_component ty i s = 290 if ((List.length (sumSyntax.strip_sum ty)) = 1) then s 291 else let val tys = sumSyntax.strip_sum ty 292 val n = List.length tys 293 val res = mk_sum_component_aux n i s 294 val tysp = split_after i tys 295 val stl = if (i=(n-1)) then [] else [(sumSyntax.list_mk_sum o List.tl) (snd tysp)] 296 val nl = if i = (n-1) then List.tabulate(n-1,fn n => n +1) else List.tabulate(n-(n-i)+1,I) 297 in inst (List.map (fn (j,t) => mk_vartype("'a"^(int_to_string j)) |-> t) 298 (ListPair.zip(List.rev nl,(fst tysp)@stl))) res 299 end 300 301(* returns s:(ty_0+ty_1+...+ty_(n-1)) tagged with OUTL's and OUTR's to strip away the sum type 302 assuming s is the i'th component in the sum *) 303fun dest_sum_component styl n i s = 304 let val _ = dbgTools.DEN dpfx "dsc" (*DBG*) 305 val _ = dbgTools.DTM (dpfx^"dsc_s") s 306 val _ = List.app (dbgTools.DTY (dpfx^"dsc_styl")) styl 307 val res = 308 if (n=1) then s (* there is only one component *) 309 else if (i = 0) then mk_comb(inst [alpha |-> List.hd styl,beta |-> list_mk_sum (List.tl styl)] outl_tm,s) 310 else if (i = 1 andalso n = 2) then mk_comb(inst [alpha |-> List.hd styl,beta |-> list_mk_sum (List.tl styl)] outr_tm,s) 311 else dest_sum_component (List.tl styl) (n-1) (i-1) (mk_comb(inst [alpha |-> List.hd styl, 312 beta |->list_mk_sum (List.tl styl)] outr_tm,s)) 313 val _ = dbgTools.DEX dpfx "dsc" (*DBG*) 314 in res end 315 316fun isIN t = let val s = term_to_string2 t in String.compare(s,"INL")=EQUAL orelse String.compare(s,"INR")=EQUAL end 317 318(* t is a term that is 1..several applications of INL/INR to some value x. Return x *) 319fun strip_in t = 320 if is_comb t 321 then let val (a,b) = dest_comb t 322 in if isIN a then strip_in b else t end 323 else t 324 325end 326end 327