utils.ml

   1 module Pa :
   2   sig
   3     val CONTEXT_TAC : ((string * pretype) list -> tactic) -> tactic
   4     val PARSE_IN_CONTEXT : (term -> tactic) -> (string -> tactic)
   5     val EXISTS_TAC : string -> tactic
   6     val SUBGOAL_THEN : string -> thm_tactic -> tactic
   7     val SUBGOAL_TAC : string -> string -> tactic list -> tactic
   8     val ASM_CASES_TAC : string -> tactic
   9     val BOOL_CASES_TAC : string -> tactic
  10     val SPEC_TAC : string * string -> tactic
  11     val SPEC : string -> thm -> thm
  12     val SPECL : string list -> thm -> thm
  13     val GEN : string -> thm -> thm
  14     val GENL : string list -> thm -> thm
  15     val X_GEN_TAC : string -> tactic
  16     val REAL_ARITH : string -> thm
  17     val REAL_FIELD : string -> thm
  18     val REAL_RING : string -> thm
  19     val ARITH_RULE : string -> thm
  20     val NUM_RING : string -> thm
  21     val INT_ARITH : string -> thm
  22     val call_with_interface : (unit -> 'a) -> (term -> 'b) -> string -> 'b
  23   end
  24   =
  25   struct
  26     let parse_preterm = fst o parse_preterm o lex o explode
  27
  28     let CONTEXT_TAC ttac (asms,c as g) =
  29       let vs = frees c @ freesl (map (concl o snd) asms) in
  30       ttac (map (fun x -> name_of x,pretype_of_type(type_of x)) vs) g
  31
  32     let PARSE_IN_CONTEXT ttac s =
  33       CONTEXT_TAC (fun env ->
  34         ttac (term_of_preterm (retypecheck env (parse_preterm s))))
  35
  36     let type_of_forall = type_of o fst o dest_forall
  37
  38     let force_type ?(env=[]) s ty =
  39       let pty = pretype_of_type ty in
  40       term_of_preterm (retypecheck env (Typing(parse_preterm s,pty)))
  41
  42     let BOOL_CONTEXT_TAC ttac s =
  43       CONTEXT_TAC (fun env -> ttac (force_type ~env s bool_ty))
  44
  45     let SUBGOAL_THEN s ttac = BOOL_CONTEXT_TAC (C SUBGOAL_THEN ttac) s
  46     let SUBGOAL_TAC l s tacs = BOOL_CONTEXT_TAC (C (SUBGOAL_TAC l) tacs) s
  47
  48     let ASM_CASES_TAC = BOOL_CONTEXT_TAC ASM_CASES_TAC
  49     let BOOL_CASES_TAC = BOOL_CONTEXT_TAC BOOL_CASES_TAC
  50
  51     let EXISTS_TAC s (_,c as g) =
  52       CONTEXT_TAC (fun env ->
  53         EXISTS_TAC (force_type ~env s (type_of (fst (dest_exists c))))) g
  54
  55     let SPEC_TAC (u,x) =
  56       PARSE_IN_CONTEXT (fun u' -> SPEC_TAC (u',force_type x (type_of u'))) u
  57
  58     let SPEC s th = SPEC (force_type s (type_of_forall (concl th))) th
  59
  60     let SPECL tms th =
  61       try rev_itlist SPEC tms th with Failure _ -> failwith "SPECL"
  62
  63     let GEN s th =
  64       GEN (try find ((=) s o name_of) (frees (concl th)) with _ -> parse_term s)
  65         th
  66
  67     let GENL = itlist GEN
  68
  69     let X_GEN_TAC s (_,c as g) = X_GEN_TAC (force_type s (type_of_forall c)) g
  70
  71     let call_with_interface p f s =
  72       let i = !the_interface in
  73       p ();
  74       let res = f (parse_term s) in
  75       the_interface := i;
  76       res
  77
  78     let [REAL_ARITH;REAL_FIELD;REAL_RING] =
  79       map (call_with_interface prioritize_real) [REAL_ARITH;REAL_FIELD;REAL_RING]
  80     let [ARITH_RULE;NUM_RING] =
  81       map (call_with_interface prioritize_num) [ARITH_RULE;NUM_RING]
  82     let INT_ARITH = call_with_interface prioritize_int INT_ARITH
  83   end;;
  84
  85 module Pa =
  86   struct
  87     include Pa
  88     let COMPLEX_FIELD = call_with_interface prioritize_complex COMPLEX_FIELD;;
  89     let SIMPLE_COMPLEX_ARITH =
  90       call_with_interface prioritize_complex SIMPLE_COMPLEX_ARITH;
  91   end;;
  92
  93 let MP_REWRITE_TAC th (_,c as g) =
  94   let [th] = mk_rewrites true th [] in
  95   let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
  96   let th = ref TRUTH in
  97   ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
  98   (SUBGOAL_THEN (lhand (concl !th)) (fun x ->
  99     REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;
 100
 101 let CASES_REWRITE_TAC th (_,c as g) =
 102   let [th] = mk_rewrites true th [] in
 103   let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
 104   let th = ref TRUTH in
 105   ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
 106   (ASM_CASES_TAC (lhand (concl !th)) THENL [
 107     POP_ASSUM (fun x -> REWRITE_TAC[MP !th x] THEN ASSUME_TAC x);
 108     POP_ASSUM (ASSUME_TAC o REWRITE_RULE[NOT_CLAUSES])]) g;;
 109
 110 let wrap f x = f [x];;
 111
 112 let CONJS xs = end_itlist CONJ xs;;
 113
 114 let rec simp_horn_conv =
 115   let is_atomic (x,y) = if x = [] then y else failwith "" in
 116   let rec tl = function [] -> [] | _::xs -> xs in
 117   fun l ->
 118     let fixpoint = ref true in
 119     let l' =
 120       rev_itlist (fun (hs,cs) (dones,todos) ->
 121         let atomics = flat (mapfilter is_atomic (dones@todos)) in
 122         let f = filter (not o C mem atomics) in
 123         let hs' = f hs and cs' = f cs in
 124         if not (hs' = hs) or not (cs' = cs) then fixpoint := false;
 125         if (cs' = [] && cs <> [])
 126         then (dones,tl todos)
 127         else ((hs',cs')::dones),tl todos)
 128       l ([],tl l)
 129     in
 130     if !fixpoint then l else simp_horn_conv (fst l');;
 131
 132 let horns_of_term =
 133   let strip_conj = binops `(/\)` in
 134   fun t -> map (fun t ->
 135     try
 136       let h,c = dest_imp t in
 137       strip_conj h,strip_conj c
 138     with _ -> [],[t]) (strip_conj t);;
 139
 140 let term_of_horns =
 141   let term_of_horn = function
 142     |[],cs -> list_mk_conj cs
 143     |_,[] -> (print_endline "ici";`T`)
 144     |hs,cs -> mk_imp (list_mk_conj hs,list_mk_conj cs)
 145   in
 146   list_mk_conj o map term_of_horn;;
 147
 148 let SIMP_HORN_CONV t =
 149   TAUT (mk_eq (t,((term_of_horns o simp_horn_conv o horns_of_term) t)));;
 150
 151 let SIMP_HORN_TAC =
 152   REWRITE_TAC[IMP_IMP]
 153   THEN CONV_TAC (TOP_DEPTH_CONV (CHANGED_CONV SIMP_HORN_CONV));;
 154
 155 let HINT_EXISTS_TAC =
 156   let strip_conj = binops `/\` in
 157   let P = `P:bool` in
 158   fun (hs,c as g) ->
 159     let hs = map snd hs in
 160     let vars = flat (map thm_frees hs) in
 161     let vs,c' = strip_exists c in
 162     let cs = strip_conj c' in
 163     let hyp_match c h = term_match (subtract vars vs) c (concl h), h in
 164     let (_,fosubs,_),h = tryfind (fun c -> tryfind (hyp_match c) hs) cs in
 165     let ts,vs' = unzip fosubs in
 166     let vs'' = subtract vs vs' in
 167     let th = MESON[] (mk_eq(list_mk_exists(vs,P),list_mk_exists(vs'@vs'',P))) in
 168     (REWRITE_TAC [th] THEN MAP_EVERY EXISTS_TAC ts THEN REWRITE_TAC [h]) g;;
 169
 170 let rec fixpoint f x =
 171   let y = f x in
 172   if y = x then y else fixpoint f y;;
 173
 174 let GIMP_IMP =
 175   GEN_ALL o REWRITE_RULE[IMP_IMP;GSYM CONJ_ASSOC] o DISCH_ALL o fixpoint
 176     (UNDISCH_ALL o SPEC_ALL);;
 177