formal_ineqs/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 (asl,w) ->
  39     let aslp = ref asl in
  40     (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
  41     (ALL_TAC (!aslp,w)));;
  42
  43 (* global_var *)
  44 let enhance flag every tac =
  45   if flag then (tac THEN every) THEN LABEL_ALL_TAC
  46    else tac;;
  47
  48 let (e_enhance :bool ->tactic->tactic ->goalstack) =
  49    fun flag every tac -> refine(by(VALID (enhance flag every tac)));;
  50
  51 (*
  52 let e_bak = e;;
  53 let every = ALL_TAC;;
  54 let e = e_enhance true every;;
  55 *)
  56
  57 let has_stv t =
  58   let typ = (type_vars_in_term t) in
  59   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
  60
  61 let enhanced_prove_by_refinement flag every (t,(tacl:tactic list)) =
  62   if (length (frees t) > 0)
  63     then failwith "prove_by_refinement: free vars" else
  64   if (has_stv t)
  65     then failwith "prove_by_refinement: has stv" else
  66   let gstate = mk_goalstate ([],t) in
  67   let _,sgs,just = rev_itlist
  68     (fun tac gs -> by  (enhance flag every tac) gs)
  69      tacl gstate in
  70   let th = if sgs = [] then just null_inst []
  71   else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  72   let t' = concl th in
  73   if t' = t then th else
  74   try EQ_MP (ALPHA t' t) th
  75   with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
  76
  77 let prove_by_refinement = enhanced_prove_by_refinement false ALL_TAC;;
  78
  79 end;;