text_formalization/jordan/refinement.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12 module Refinement = struct
  13
  14 (* ------------------------------------------------------------------ *)
  15 (* This bundles an interactive session into a proof. *)
  16 (* Later split off into general/prove_by_refinement *)
  17 (* ------------------------------------------------------------------ *)
  18
  19 (*
  20 let labels_flag = ref false;; (* if true add labels to assumptions *)
  21 *)
  22
  23 let LABEL_ALL_TAC:tactic =
  24  let mk_label avoid =
  25   let rec mk_one_label i avoid  =
  26     let label = "Z-"^(string_of_int i) in
  27       if not(mem label avoid) then label else mk_one_label (i+1) avoid in
  28     mk_one_label 0 avoid in
  29  let update_label i asl =
  30   let rec f_at_i f j =
  31     function [] -> []
  32       | a::b -> if (j=0) then (f a)::b else a::(f_at_i f (j-1) b) in
  33   let avoid = map fst asl in
  34   let current = el i avoid in
  35   let new_label = mk_label avoid in
  36   if (String.length current > 0) then asl else
  37     f_at_i (fun (_,y) -> (new_label,y) ) i asl in
  38   fun gl  ->
  39     let (asl,w) = dest_goal gl in
  40     let aslp = ref asl in
  41     (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
  42     (ALL_TAC (mk_goal(!aslp,w))));;
  43
  44 (* global_var *)
  45 let enhance flag every tac =
  46   if flag then (tac THEN every) THEN LABEL_ALL_TAC
  47    else tac;;
  48
  49 let (e_enhance :bool ->tactic->tactic ->goalstack) =
  50    fun flag every tac -> refine(by(VALID (enhance flag every tac)));;
  51
  52 (*
  53 let e_bak = e;;
  54 let every = ALL_TAC;;
  55 let e = e_enhance true every;;
  56 *)
  57
  58 let has_stv t =
  59   let typ = (type_vars_in_term t) in
  60   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
  61
  62 let enhanced_prove_by_refinement flag every (t,(tacl:tactic list)) =
  63   if (length (frees t) > 0)
  64     then failwith "prove_by_refinement: free vars" else
  65   if (has_stv t)
  66     then failwith "prove_by_refinement: has stv" else
  67   let gstate = mk_goalstate ([],t) in
  68   let _,sgs,just = rev_itlist
  69     (fun tac gs -> by  (enhance flag every tac) gs)
  70      tacl gstate in
  71   let th = if sgs = [] then just null_inst []
  72   else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  73   let t' = concl th in
  74   if t' = t then th else
  75   try EQ_MP (ALPHA t' t) th
  76   with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
  77
  78 let prove_by_refinement = enhanced_prove_by_refinement false ALL_TAC;;
  79
  80 end;;