text_formalization/general/prove_by_refinement.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* prove_by_refinement                                                    *)
   5 (* Chapter: General                                                        *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11
  12 This is an alternative to "prove"
  13 Instead of chaining tactics together with THEN and THENL,
  14 a list is given of all the tactics used, in the exact same order as the sequence of steps used with "e"
  15
  16 The advantage of this over "prove" is that the list exactly matches the sequence of steps with "e".
  17 There is no need to reorganize the interactive proof by working out what branches were followed
  18 when multiple goals are in play.
  19
  20 The navigation commands are for a proof set up with prove_by_step.  It allows one to step
  21 through the tactics in the tactic list one-by-one for purposes of debugging.
  22
  23 *)
  24
  25
  26
  27 module type Prove_by_refinement_type = sig
  28
  29   val prove_by_refinement : term*(tactic list) -> thm
  30   val prove_by_refinement_2 : string*term*(tactic list) -> thm
  31
  32 (*
  33   val prove_by_step : term*(tactic list) -> goalstack
  34 *)
  35
  36 (* navigation of prove_by_step: *)
  37
  38 (*
  39   val e' : unit -> goalstack (* one step forward *)
  40   val f' : int -> goalstack (* n steps forward *)
  41   val b' : unit -> goalstack (* one step backwards *)
  42   val p' : unit -> goalstack  (* print goalstack *)
  43   val r' : unit -> goalstack (* revert to original goal *)
  44   val n' : unit -> int (* number of next step *)
  45   val l' : unit -> int (* total number of steps *)
  46   val x' : unit -> int (* step position of next error *)
  47 *)
  48
  49 end;;
  50
  51
  52 module Prove_by_refinement : Prove_by_refinement_type = struct
  53
  54
  55
  56 (* adapted from
  57 hol_til_2005/HOL_TIL_2005/FLYSPECK_PUB_9_2004/hol_light_o/hol-ext/tactics_2.ml
  58 :prove_by_refinement *)
  59
  60
  61
  62   let prove_by_refinement(t,(tacl:tactic list)) =
  63     let gstate = mk_goalstate ([],t) in
  64     let _,sgs,just = rev_itlist
  65       (fun tac gs -> by
  66          (tac) gs)
  67       tacl gstate in
  68     let th = if sgs = [] then just null_inst []
  69     else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  70     let t' = concl th in
  71       if t' = t then th else
  72         try EQ_MP (ALPHA t' t) th
  73         with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
  74
  75   let prove_by_refinement_2(thm_name,t,(tacl:tactic list)) =
  76     let gstate = mk_goalstate ([],t) in
  77     let ctacl = zip (0--(List.length tacl -1)) tacl in
  78     let _,sgs,just = rev_itlist
  79       (fun (i,tac) gs ->
  80          try by
  81            (tac) gs
  82          with Failure s ->
  83            let _ = print_goalstack ([gs]) in
  84            let _ = report ("Proof of "^thm_name^" fails at step: "^(string_of_int i)) in
  85              failwith s
  86       )
  87       ctacl gstate in
  88     let th = if sgs = [] then just null_inst []
  89     else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  90     let t' = concl th in
  91       if t' = t then th else
  92         try EQ_MP (ALPHA t' t) th
  93         with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
  94
  95
  96 (* replaying proof by refinement *)
  97
  98 (*
  99   let tl = ref ([]:tactic list);;
 100   let step = ref 0;;
 101   let gtm = ref `T`;;
 102
 103   let g_step t = (step:=0; gtm := t; g t);;
 104   let e_step() = let gs = e(List.nth (!tl) (!step)) in (step:= (!step + 1);gs);;
 105   let rec f_step n = if (n<=0) then p() else if (n=1) then e_step() else f_step (n-1);;
 106   let p_step() =p();;
 107   let get_step() = (!step);;
 108   let get_steplength() = List.length (!tl);;
 109
 110   let b_step() =
 111     if (!step <= 0) then failwith "Can't back up any more"
 112     else let gs = b() in (step:= (!step -1);gs);;
 113
 114   let rec next_error () = if (!step >= List.length (!tl)) then (!step) else
 115     try ((let _ = e(List.nth (!tl) (!step)) in () ) ; step:= (!step + 1);next_error())
 116     with Failure _ -> (!step);;
 117
 118   let prove_by_step (gl,t) =
 119     (tl := t;g_step gl);;
 120   let r_step () = (prove_by_step (!gtm,!tl));;  (* revert *)
 121
 122   let (e',f',b',p',r',n',l',x') = (e_step,f_step,b_step,p_step,r_step,get_step,get_steplength,next_error);;
 123 *)
 124
 125 end;;