2 (* miscellaneous useful stuff that doesn't fit in anywhere else *)
4 let pair_map f (x,y) = (f x,f y)
6 (* module for maps keyed on terms *)
7 module Termmap = Map.Make (struct type t = term let compare = Pervasives.compare end)
9 module Litset = Set.Make (struct type t = bool * int let compare = Pervasives.compare end)
11 let tm_listItems m = List.rev (Termmap.fold (fun k v l -> (k,v)::l) m [])
13 let print_term t = print_string (string_of_term t)
15 let print_type ty = print_string (string_of_type ty)
17 (*FIXME: inefficient to read chars one by one; 1024 can be improved upon*)
21 (try Some (input_char in_ch)
22 with End_of_file -> None)
24 Some c -> (Buffer.add_char b c; loop b)
26 let b = Buffer.create 1024 in
30 let QUANT_CONV conv = RAND_CONV(ABS_CONV conv)
32 let BINDER_CONV conv = ABS_CONV conv ORELSEC QUANT_CONV conv
34 let rec LAST_FORALL_CONV c tm =
35 if is_forall (snd (dest_forall tm))
37 BINDER_CONV (LAST_FORALL_CONV c) tm
40 let FORALL_IMP_CONV tm =
41 let (bvar,bbody) = dest_forall tm in
42 let (ant,conseq) = dest_imp bbody in
43 let fant = free_in bvar ant in
44 let fconseq = free_in bvar conseq in
45 let ant_thm = ASSUME ant in
46 let tm_thm = ASSUME tm in
48 then failwith("FORALL_IMP_CONV"^
49 ("`"^(fst(dest_var bvar))^"` free on both sides of `==>`"))
53 let asm = mk_exists(bvar,ant) in
54 let th1 = CHOOSE(bvar,ASSUME asm) (UNDISCH(SPEC bvar tm_thm)) in
55 let imp1 = DISCH tm (DISCH asm th1) in
56 let cncl = rand(concl imp1) in
57 let th2 = MP (ASSUME cncl) (EXISTS (asm,bvar) ant_thm) in
58 let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in
59 IMP_ANTISYM_RULE imp1 imp2
63 let imp1 = DISCH ant(GEN bvar(UNDISCH(SPEC bvar tm_thm))) in
64 let cncl = concl imp1 in
65 let imp2 = GEN bvar(DISCH ant(SPEC bvar(UNDISCH(ASSUME cncl)))) in
66 IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2)
68 let asm = mk_exists(bvar,ant) in
69 let tmp = UNDISCH (SPEC bvar tm_thm) in
70 let th1 = GEN bvar (CHOOSE(bvar,ASSUME asm) tmp) in
71 let imp1 = DISCH tm (DISCH asm th1) in
72 let cncl = rand(concl imp1) in
73 let th2 = SPEC bvar (MP(ASSUME cncl) (EXISTS (asm,bvar) ant_thm)) in
74 let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in
75 IMP_ANTISYM_RULE imp1 imp2
77 let LEFT_IMP_EXISTS_CONV tm =
78 let ant, _ = dest_imp tm in
79 let bvar,bdy = dest_exists ant in
80 let x' = variant (frees tm) bvar in
81 let t' = subst [x',bvar] bdy in
82 let th1 = GEN x' (DISCH t'(MP(ASSUME tm)(EXISTS(ant,x')(ASSUME t')))) in
83 let rtm = concl th1 in
84 let th2 = CHOOSE (x',ASSUME ant) (UNDISCH(SPEC x'(ASSUME rtm))) in
85 IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2))
89 (*********** terms **************)
91 let lrand x = rand (rator x)
96 let is_T tm = (tm = t_tm)
98 let is_F tm = (tm = f_tm)
100 (************ HOL **************)
105 let ((ltl,ltr),(tml,tmr)) =
106 pair_map dest_comb (lt,tm) in
107 (ERC ltl tml)@(ERC ltr tmr)
113 (* easier REWR_CONV which assumes that the supplied theorem is ground and quantifier free,
114 so type instantiation and var capture checks are not needed *)
115 (* no restrictions on the term argument *)
116 let EREWR_CONV th tm =
117 let lt = lhs(concl th) in
118 let il = ERC lt tm in