1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* prove_by_refinement *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
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"
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.
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.
27 module type Prove_by_refinement_type = sig
29 val prove_by_refinement : term*(tactic list) -> thm
30 val prove_by_refinement_2 : string*term*(tactic list) -> thm
33 val prove_by_step : term*(tactic list) -> goalstack
36 (* navigation of prove_by_step: *)
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 *)
52 module Prove_by_refinement : Prove_by_refinement_type = struct
57 hol_til_2005/HOL_TIL_2005/FLYSPECK_PUB_9_2004/hol_light_o/hol-ext/tactics_2.ml
58 :prove_by_refinement *)
62 let prove_by_refinement(t,(tacl:tactic list)) =
63 let gstate = mk_goalstate ([],t) in
64 let _,sgs,just = rev_itlist
68 let th = if sgs = [] then just null_inst []
69 else failwith "BY_REFINEMENT_PROOF: Unsolved goals" 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";;
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
83 let _ = print_goalstack ([gs]) in
84 let _ = report ("Proof of "^thm_name^" fails at step: "^(string_of_int i)) in
88 let th = if sgs = [] then just null_inst []
89 else failwith "BY_REFINEMENT_PROOF: Unsolved goals" 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";;
96 (* replaying proof by refinement *)
99 let tl = ref ([]:tactic list);;
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);;
107 let get_step() = (!step);;
108 let get_steplength() = List.length (!tl);;
111 if (!step <= 0) then failwith "Can't back up any more"
112 else let gs = b() in (step:= (!step -1);gs);;
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);;
118 let prove_by_step (gl,t) =
119 (tl := t;g_step gl);;
120 let r_step () = (prove_by_step (!gtm,!tl));; (* revert *)
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);;