(* miscellaneous useful stuff that doesn't fit in anywhere else *) let pair_map f (x,y) = (f x,f y) (* module for maps keyed on terms *) module Termmap = Map.Make (struct type t = term let compare = Pervasives.compare end) module Litset = Set.Make (struct type t = bool * int let compare = Pervasives.compare end) let tm_listItems m = List.rev (Termmap.fold (fun k v l -> (k,v)::l) m []) let print_term t = print_string (string_of_term t) let print_type ty = print_string (string_of_type ty) (*FIXME: inefficient to read chars one by one; 1024 can be improved upon*) let input_all in_ch = let rec loop b = match (try Some (input_char in_ch) with End_of_file -> None) with Some c -> (Buffer.add_char b c; loop b) | None -> () in let b = Buffer.create 1024 in let _ = loop b in Buffer.contents b let QUANT_CONV conv = RAND_CONV(ABS_CONV conv) let BINDER_CONV conv = ABS_CONV conv ORELSEC QUANT_CONV conv let rec LAST_FORALL_CONV c tm = if is_forall (snd (dest_forall tm)) then BINDER_CONV (LAST_FORALL_CONV c) tm else c tm let FORALL_IMP_CONV tm = let (bvar,bbody) = dest_forall tm in let (ant,conseq) = dest_imp bbody in let fant = free_in bvar ant in let fconseq = free_in bvar conseq in let ant_thm = ASSUME ant in let tm_thm = ASSUME tm in if (fant && fconseq) then failwith("FORALL_IMP_CONV"^ ("`"^(fst(dest_var bvar))^"` free on both sides of `==>`")) else if fant then let asm = mk_exists(bvar,ant) in let th1 = CHOOSE(bvar,ASSUME asm) (UNDISCH(SPEC bvar tm_thm)) in let imp1 = DISCH tm (DISCH asm th1) in let cncl = rand(concl imp1) in let th2 = MP (ASSUME cncl) (EXISTS (asm,bvar) ant_thm) in let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in IMP_ANTISYM_RULE imp1 imp2 else if fconseq then let imp1 = DISCH ant(GEN bvar(UNDISCH(SPEC bvar tm_thm))) in let cncl = concl imp1 in let imp2 = GEN bvar(DISCH ant(SPEC bvar(UNDISCH(ASSUME cncl)))) in IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2) else let asm = mk_exists(bvar,ant) in let tmp = UNDISCH (SPEC bvar tm_thm) in let th1 = GEN bvar (CHOOSE(bvar,ASSUME asm) tmp) in let imp1 = DISCH tm (DISCH asm th1) in let cncl = rand(concl imp1) in let th2 = SPEC bvar (MP(ASSUME cncl) (EXISTS (asm,bvar) ant_thm)) in let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in IMP_ANTISYM_RULE imp1 imp2 let LEFT_IMP_EXISTS_CONV tm = let ant, _ = dest_imp tm in let bvar,bdy = dest_exists ant in let x' = variant (frees tm) bvar in let t' = subst [x',bvar] bdy in let th1 = GEN x' (DISCH t'(MP(ASSUME tm)(EXISTS(ant,x')(ASSUME t')))) in let rtm = concl th1 in let th2 = CHOOSE (x',ASSUME ant) (UNDISCH(SPEC x'(ASSUME rtm))) in IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2)) (*********** terms **************) let lrand x = rand (rator x) let t_tm = `T`;; let f_tm = `F`;; let is_T tm = (tm = t_tm) let is_F tm = (tm = f_tm) (************ HOL **************) let rec ERC lt tm = if is_comb lt then let ((ltl,ltr),(tml,tmr)) = pair_map dest_comb (lt,tm) in (ERC ltl tml)@(ERC ltr tmr) else if is_var lt then [(tm,lt)] else [] (* easier REWR_CONV which assumes that the supplied theorem is ground and quantifier free, so type instantiation and var capture checks are not needed *) (* no restrictions on the term argument *) let EREWR_CONV th tm = let lt = lhs(concl th) in let il = ERC lt tm in INST il th