jHOLLight/caml/sections.hl

   1 module Sections = struct
   2
   3 (* Basic commands for working with the goal stack *)
   4 (* b() from tactics.ml *)
   5 let revert_proof_step() =
   6   let l = !current_goalstack in
   7     if length l = 1 then failwith "Can't back up any more" else
   8       current_goalstack := tl l;
   9     !current_goalstack;;
  10
  11
  12 (* A flag for fast proof loading (using mk_thm) *)
  13 let fast_load_flag = ref false;;
  14
  15 (* Section variables, hypotheses (with labels), implicit types, and auxiliary lemmas *)
  16 type section_info =
  17 {
  18   vars : term list;
  19   hyps : (string * term) list;
  20   types : (string * hol_type) list;
  21   lemmas : (string * thm) list;
  22 };;
  23
  24
  25 let empty_section : section_info = {vars = []; hyps = []; types = []; lemmas = []};;
  26
  27 let section_stack = ref ([] : (string * section_info ref) list);;
  28
  29
  30 (* Begins a new section *)
  31 let begin_section name =
  32   let sections = !section_stack in
  33     if can (C assoc sections) name then
  34       failwith ("Section " ^ name ^ " is already active")
  35     else
  36       let sections = (name, ref empty_section) :: sections in
  37       section_stack := sections;;
  38
  39
  40 (* Ends the active section *)
  41 let end_section name =
  42   let sections = !section_stack in
  43     if sections = [] then
  44       failwith "end_section: No open sections"
  45     else
  46       let last_name, _ = hd sections in
  47         if Pervasives.compare last_name name <> 0 then
  48           failwith ("The last open section is " ^ last_name)
  49         else
  50           section_stack := tl sections;;
  51
  52
  53 (* Ends all sections *)
  54 let end_all_sections () =
  55   section_stack := [];;
  56
  57
  58 (* Returns all section variables in the current section *)
  59 let current_section_vars () =
  60   if !section_stack = [] then []
  61   else
  62     !((snd o hd) !section_stack).vars;;
  63
  64
  65 (* Returns all hypotheses in the current section *)
  66 let current_section_hyps () =
  67   if !section_stack = [] then []
  68   else
  69     !((snd o hd) !section_stack).hyps;;
  70
  71
  72 (* Returns all section variables from all sections *)
  73 let section_vars () : term list =
  74   let vars = map (fun (_, s) -> !s.vars) !section_stack in
  75     List.concat vars;;
  76
  77
  78 (* Returns all implicit types from all sections *)
  79 let section_types () : (string * hol_type) list =
  80   let types = map (fun (_, s) -> !s.types) !section_stack in
  81     List.concat types;;
  82
  83
  84 (* Returns all hypotheses from all sections *)
  85 let section_hyps () : (string * term) list =
  86   let hyps = map (fun (_, s) -> !s.hyps) !section_stack in
  87     List.concat hyps;;
  88
  89
  90 (* Returns all lemmas from all sections *)
  91 let section_lemmas () : (string * thm) list =
  92   let lemmas = map (fun (_, s) -> !s.lemmas) !section_stack in
  93     List.concat lemmas;;
  94
  95
  96 (* Returns names of all section lemmas and hypotheses *)
  97 let section_labels () : string list =
  98   let hyp_names = map fst (section_hyps()) and
  99       lemma_names = map fst (section_lemmas()) in
 100     hyp_names @ lemma_names;;
 101
 102
 103 (* Instantiates types of section variables in the term *)
 104 let inst_section_vars tm =
 105   let s_vars = map dest_var (section_vars()) in
 106   let find_var (name, ty) =
 107     try (assoc name s_vars, ty)
 108     with Failure _ -> (bool_ty, bool_ty) in
 109   let inst_var (name, ty) tm =
 110     let ty_dst, ty_src = find_var (name, ty) in
 111       try (inst (type_match ty_src ty_dst []) tm)
 112       with Failure _ ->
 113         failwith ("Section variable " ^ name ^
 114                     " has type " ^ string_of_type ty_dst) in
 115   let f_vars = map dest_var (frees tm) in
 116     itlist inst_var f_vars tm;;
 117
 118
 119 (* Instantiates implicit types in the given term *)
 120 (* (free variables and top generalized variables are considered in the term) *)
 121 let inst_section_types tm =
 122   let s_types = section_types() in
 123   let find_type tm =
 124     let name, ty = dest_var tm in
 125     try (assoc name s_types, ty) with Failure _ -> (bool_ty, bool_ty) in
 126   let f_vars = frees tm in
 127   let g_vars, _ = strip_forall tm in
 128   let ty_dst, ty_src = unzip (map find_type (g_vars @ f_vars)) in
 129   let ty_inst = itlist2 type_match ty_src ty_dst [] in
 130     inst ty_inst tm;;
 131
 132
 133 (* Checks if the term contains any free variables
 134    which are not section variables *)
 135 let check_section_term tm =
 136   let f_vars = frees tm in
 137   if !section_stack = [] then
 138     if f_vars <> [] then
 139       let str = String.concat ", " (map string_of_term f_vars) in
 140         failwith ("Free variables: " ^ str)
 141     else ()
 142   else
 143     let s_vars = section_vars() in
 144     let vars = subtract f_vars s_vars in
 145       if vars <> [] then
 146         let str = String.concat ", " (map string_of_term vars) in
 147           failwith ("Free variables: " ^ str)
 148       else ();;
 149
 150
 151 (* Adds the given variable to the active section *)
 152 let add_section_var var =
 153   let sections = !section_stack in
 154     if sections = [] then
 155       failwith "add_section_var: No open sections"
 156     else
 157       let s_var = section_vars() in
 158       let var_name, _ = dest_var var in
 159         if can (C assoc (map dest_var s_var)) var_name then
 160           failwith ("A variable with the name "^var_name^" is already defined")
 161         else
 162           let section = (snd o hd) sections in
 163             section := {!section with vars = var :: !section.vars};;
 164
 165
 166 (* Adds the given implicit type to the active section *)
 167 let add_section_type tm =
 168   let sections = !section_stack in
 169     if sections = [] then
 170       failwith "add_section_type: No open sections"
 171     else
 172       let s_types = section_types() in
 173       let var_name, ty = dest_var tm in
 174         if can (C assoc s_types) var_name then
 175           failwith ("An implicit type for the variable "^var_name^" is already defined")
 176         else
 177           let section = (snd o hd) sections in
 178             section := {!section with types = (var_name, ty) :: !section.types};;
 179
 180 (* Adds the given lemma to the active section *)
 181 let add_section_lemma name th =
 182   let sections = !section_stack in
 183     if sections = [] then
 184       failwith "add_section_lemma: No open sections"
 185     else
 186       let labels = section_labels() in
 187         if mem name labels then
 188           failwith ("A lemma (or hypothesis) with the name " ^ name ^ " is already defined")
 189         else
 190           let section = (snd o hd) sections in
 191             section := {!section with lemmas = (name, th) :: !section.lemmas};;
 192
 193
 194 (* Adds the given hypothesis (term) to the active section *)
 195 let add_section_hyp label hyp =
 196   let sections = !section_stack in
 197     if sections = [] then
 198       failwith "add_section_hyp: No open sections"
 199     else
 200       let labels = section_labels() in
 201         if mem label labels then
 202           failwith ("A hypothesis (or lemma) with the label " ^ label ^ " is already defined")
 203         else
 204           let hyp0 = inst_section_vars hyp in
 205           let hyp1 = inst_section_types hyp0 in
 206           if type_of hyp1 <> bool_ty then
 207             failwith "A boolean term is expected"
 208           else
 209             let section = (snd o hd) sections in
 210               check_section_term hyp1;
 211               section := {!section with hyps = (label, hyp1) :: !section.hyps};;
 212
 213
 214 (* Removes the given variable from the active section *)
 215 let remove_section_var var_name =
 216   let sections = !section_stack in
 217     if sections = [] then
 218       failwith "remove_section_var: No open sections"
 219     else
 220       let section = (snd o hd) sections in
 221       let new_vars = filter (fun var -> (fst o dest_var) var <> var_name) !section.vars in
 222         section := {!section with vars = new_vars};;
 223
 224
 225 (* Removes the given implicit type from the active section *)
 226 let remove_section_type type_name =
 227   let sections = !section_stack in
 228     if sections = [] then
 229       failwith "remove_section_type: No open sections"
 230     else
 231       let section = (snd o hd) sections in
 232       let new_types = filter (fun name, _ -> name <> type_name) !section.types in
 233         section := {!section with types = new_types};;
 234
 235
 236 (* Removes the given lemma from the active section *)
 237 let remove_section_lemma lemma_name =
 238   let sections = !section_stack in
 239     if sections = [] then
 240       failwith "remove_section_lemma: No open sections"
 241     else
 242       let section = (snd o hd) sections in
 243       let new_lemmas = filter (fun name, _ -> name <> lemma_name) !section.lemmas in
 244         section := {!section with lemmas = new_lemmas};;
 245
 246
 247 (* Removes the given assumption from the active section *)
 248 let remove_section_hyp label =
 249   let sections = !section_stack in
 250     if sections = [] then
 251       failwith "remove_section_hyp: No open sections"
 252     else
 253       let section = (snd o hd) sections in
 254       let new_hyps = filter (fun name, _ -> name <> label) !section.hyps in
 255         section := {!section with hyps = new_hyps};;
 256
 257
 258 (* Prepares a goal term *)
 259 let prepare_goal_term tm =
 260   if !section_stack = [] then (check_section_term tm; tm)
 261   else
 262     let tm0 = inst_section_vars tm in
 263     let tm1 = inst_section_types tm0 in
 264     let s_hyps = map snd (section_hyps()) in
 265     let r = itlist (curry mk_imp) s_hyps tm1 in
 266       check_section_term r; r;;
 267
 268
 269 (* Prepares a goal term and an initial tactic *)
 270 let prepare_section_proof names tm =
 271   let f_vars = map dest_var (frees tm) in
 272   let find_type var_name =
 273     try assoc var_name f_vars with Failure _ -> failwith ("Unused variable: " ^ var_name) in
 274   let g_vars = map (fun name -> mk_var (name, find_type name)) names in
 275   let g_tm = list_mk_forall (g_vars, tm) in
 276   let tm0 = prepare_goal_term g_tm in
 277   let hyp_names = map fst (section_hyps()) in
 278   let lemmas = section_lemmas() in
 279   let gen_tac = REPLICATE_TAC (length g_vars) GEN_TAC in
 280   let disch_tac = itlist (fun name tac -> DISCH_THEN (LABEL_TAC name) THEN tac) hyp_names ALL_TAC in
 281   let assume_tac = itlist (fun (name,lemma) tac -> LABEL_TAC name lemma THEN tac) lemmas ALL_TAC in
 282     tm0, assume_tac THEN disch_tac THEN gen_tac;;
 283
 284
 285 (* Starts a proof of the goal using section hypotheses *)
 286 let start_section_proof names tm =
 287   let tm0, tac0 = prepare_section_proof names tm in
 288   let _ = set_goal([], tm0) in
 289     refine (by (VALID tac0));;
 290
 291
 292 (* Returns the final theorem *)
 293 let end_section_proof () =
 294   let th = top_thm() in
 295   let hyps = section_hyps() in
 296     itlist (fun _ th -> UNDISCH th) hyps th;;
 297
 298
 299 (* Proves a lemma using section hypotheses and variables *)
 300 let section_proof names tm tac_list =
 301   let tm0, tac0 = prepare_section_proof names tm in
 302   let gstate = mk_goalstate ([], tm0) in
 303   let tac_list1 =
 304     if !fast_load_flag then
 305       [fun g -> ACCEPT_TAC(mk_thm([], snd g)) g]
 306     else
 307       tac_list in
 308   let _, sgs, just = rev_itlist by (tac0 :: tac_list1) gstate in
 309   let th0 =
 310     if sgs = [] then just null_inst []
 311     else failwith "section_proof: unsolved goals" in
 312   let hyps = section_hyps() in
 313     itlist (fun _ th -> UNDISCH th) hyps th0;;
 314
 315
 316 (* Discharges all assumptions and generalizes all section variables *)
 317 let finalize_theorem th =
 318   let hyps = map snd (current_section_hyps()) in
 319   let th_hyps = hyp th in
 320   let hyps0 = intersect hyps th_hyps in
 321   let s_vars = current_section_vars() in
 322   let th1 = rev_itlist (fun hyp th -> DISCH hyp th) hyps0 th in
 323   let f_vars = frees (concl th1) in
 324   let vars = intersect f_vars s_vars in
 325     itlist (fun var th -> GEN var th) vars th1;;
 326
 327 end;;