(******************************************************************************)
(* FILE          : environment.ml                                             *)
(* DESCRIPTION   : Environment of definitions and pre-proved theorems for use *)
(*                 in automation.                                             *)
(*                                                                            *)
(* READS FILES   : <none>                                                     *)
(* WRITES FILES  : <none>                                                     *)
(*                                                                            *)
(* AUTHOR        : R.J.Boulton                                                *)
(* DATE          : 8th May 1991                                               *)
(*                                                                            *)
(* LAST MODIFIED : R.J.Boulton                                                *)
(* DATE          : 12th October 1992                                          *)
(*                                                                            *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
(* DATE          : July 2009                                                  *)
(******************************************************************************)

let my_gen_terms = ref ([]:term list);;
let bm_steps = ref (0,0);;


let rec GSPEC th =
  let wl,w = dest_thm th in
  if is_forall w then
      GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th)
  else th;;

let LIST_CONJ = end_itlist CONJ ;;

let rec CONJ_LIST n th =
  try if n=1 then [th] else (CONJUNCT1 th)::(CONJ_LIST (n-1) (CONJUNCT2 th))
  with Failure _ -> failwith "CONJ_LIST";;

(*----------------------------------------------------------------------------*)
(* Reference variable to hold the defining theorems for operators currently   *)
(* defined within the system. Each definition is stored as a triple. The      *)
(* first component is the name of the operator. The second is the number of   *)
(* the recursive argument. If the operator is not defined recursively, this   *)
(* number is zero. The third component is a list of pairs of type constructor *)
(* names and the theorems that define the behaviour of the operator for each  *)
(* constructor. If the operator is not recursive, the constructor names are   *)
(* empty (null) strings.                                                      *)
(*----------------------------------------------------------------------------*)

let system_defs = ref ([] : (string * (int * (string * thm) list)) list);;

(*----------------------------------------------------------------------------*)
(* new_def : thm -> void                                                      *)
(*                                                                            *)
(* Make a new definition available. Checks that theorem has no hypotheses,    *)
(* then splits it into conjuncts. The variables for each conjunct are         *)
(* specialised and then the conjuncts are made into equations.                *)
(*                                                                            *)
(* For each equation, a triple is obtained, consisting of the name of the     *)
(* function on the LHS, the number of the recursive argument, and the name of *)
(* the constructor used in that argument. This process fails if the LHS is    *)
(* not an application of a constant (possibly to zero arguments), or if more  *)
(* than one of the arguments is anything other than a variable. The argument  *)
(* that is not a variable must be an application of a constructor. If the     *)
(* function is not recursive, the argument number returned is zero.           *)
(*                                                                            *)
(* Having obtained a triple for each equation, a check is made that the first *)
(* two components are the same for each equation. Then, the equations are     *)
(* saved together with constructor names for each, and the name of the        *)
(* operator being defined, and the number of the recursive argument.          *)
(*----------------------------------------------------------------------------*)

let new_def th =
try 
 (let make_into_eqn th =
     let tm = concl th
     in  if (is_eq tm) then th
         else if (is_neg tm) then EQF_INTRO th
         else EQT_INTRO th
  and get_constructor th =
     let tm = lhs (concl th)
     in  let (f,args) = strip_comb tm
     in  let name = fst (dest_const f)
     in  let bools = number_list (map is_var args)
     in  let i = itlist (fun (b,i) n -> if ((not b) & (n = 0)) then i
                                   else if b then n else failwith "") bools 0
     in  if (i = 0)
         then ((name,i),"")
         else ((name,i),fst (dest_const (fst (strip_comb (el (i-1) args)))))
  in  let ([],tm) = dest_thm th
  in  let ths = CONJ_LIST (length (conj_list tm)) th
  in  let ths' = map SPEC_ALL ths
  in  let eqs = map make_into_eqn ths'
  in  let constructs = map get_constructor eqs
  in  let (xl,yl) = hashI setify (List.split constructs)
  in  let (name,i) = if (length xl = 1) then (hd xl) else failwith ""
  in  system_defs := (name,(i,List.combine yl eqs))::(!system_defs)
 ) with Failure _ -> failwith "new_def";;

(*----------------------------------------------------------------------------*)
(* defs : void -> thm list list                                               *)
(*                                                                            *)
(* Returns a list of lists of theorems currently being used as definitions.   *)
(* Each list in the list is for one operator.                                 *)
(*----------------------------------------------------------------------------*)

let defs () = map ((map snd) o snd o snd) (!system_defs);;
let defs_names () = map fst (!system_defs);;

(*----------------------------------------------------------------------------*)
(* get_def : string -> (string # int # (string # thm) list)                   *)
(*                                                                            *)
(* Function to obtain the definition information of a named operator.         *)
(*----------------------------------------------------------------------------*)

let get_def name = try ( assoc name (!system_defs) ) with Failure _ -> failwith "get_def";;

(*----------------------------------------------------------------------------*)
(* Reference variable for a list of theorems currently proved in the system.  *)
(* These theorems are available to the automatic proof procedures for use as  *)
(* rewrite rules. The elements of the list are actually pairs of theorems.    *)
(* The first theorem is that specified by the user. The second is an          *)
(* equivalent theorem in a standard form.                                     *)
(*----------------------------------------------------------------------------*)

let system_rewrites = ref ([] : (thm * thm) list);;

(*----------------------------------------------------------------------------*)
(* CONJ_IMP_IMP_IMP = |- x /\ y ==> z = x ==> y ==> z                         *)
(*----------------------------------------------------------------------------*)

let CONJ_IMP_IMP_IMP = 
prove (`((x /\ y) ==> z) = (x ==> (y ==> z))`,
BOOL_CASES_TAC `x:bool` THEN BOOL_CASES_TAC `y:bool` THEN BOOL_CASES_TAC `z:bool` THEN REWRITE_TAC []);;
(*----------------------------------------------------------------------------*) (* CONJ_UNDISCH : thm -> thm *) (* *) (* Undischarges the conjuncts of the antecedant of an implication. *) (* e.g. |- x /\ (y /\ z) /\ w ==> x ---> x, y /\ z, w |- x *) (* *) (* Has to check for negations, because UNDISCH processes them when we don't *) (* want it to. *) (*----------------------------------------------------------------------------*) let rec CONJ_UNDISCH th = try (let th' = CONV_RULE (REWR_CONV CONJ_IMP_IMP_IMP) th in let th'' = UNDISCH th' in CONJ_UNDISCH th'') with Failure _ -> try (if not (is_neg (concl th)) then UNDISCH th else failwith "") with Failure _ -> failwith "CONJ_UNDISCH";; (*----------------------------------------------------------------------------*) (* new_rewrite_rule : thm -> void *) (* *) (* Make a new rewrite rule available. Checks that theorem has no hypotheses. *) (* The theorem is saved together with an equivalent theorem in a standard *) (* form. Theorems are fully generalized, then specialized with unique *) (* variable names (genvars), and then standardized as follows: *) (* *) (* |- (h1 /\ ... /\ hn) ==> (l = r) ---> h1, ..., hn |- l = r *) (* |- (h1 /\ ... /\ hn) ==> ~b ---> h1, ..., hn |- b = F *) (* |- (h1 /\ ... /\ hn) ==> b ---> h1, ..., hn |- b = T *) (* |- l = r ---> |- l = r *) (* |- ~b ---> |- b = F *) (* |- b ---> |- b = T *) (* *) (* A conjunction of rules may be given. The function will treat each conjunct *) (* in the theorem as a separate rule. *) (*----------------------------------------------------------------------------*) let rec new_rewrite_rule th = try (if (is_conj (concl th)) then (map new_rewrite_rule (CONJUNCTS th); ()) else let ([],tm) = dest_thm th in let th' = GSPEC (GEN_ALL th) in let th'' = try (CONJ_UNDISCH th') with Failure _ -> th' in let tm'' = concl th'' in let th''' = (if (is_eq tm'') then th'' else if (is_neg tm'') then EQF_INTRO th'' else EQT_INTRO th'') in system_rewrites := (th,th''')::(!system_rewrites) ) with Failure _ -> failwith "new_rewrite_rule";; (*----------------------------------------------------------------------------*) (* rewrite_rules : void -> thm list *) (* *) (* Returns the list of theorems currently being used as rewrites, in the form *) (* they were originally given by the user. *) (*----------------------------------------------------------------------------*) let rewrite_rules () = map fst (!system_rewrites);; (*----------------------------------------------------------------------------*) (* Reference variable to hold the generalisation lemmas currently known to *) (* the system. *) (*----------------------------------------------------------------------------*) let system_gen_lemmas = ref ([] : thm list);; (*----------------------------------------------------------------------------*) (* new_gen_lemma : thm -> void *) (* *) (* Make a new generalisation lemma available. *) (* Checks that the theorem has no hypotheses. *) (*----------------------------------------------------------------------------*) let new_gen_lemma th = if ((hyp th) = []) then system_gen_lemmas := th::(!system_gen_lemmas) else failwith "new_gen_lemma";; (*----------------------------------------------------------------------------*) (* gen_lemmas : void -> thm list *) (* *) (* Returns the list of theorems currently being used as *) (* generalisation lemmas. *) (*----------------------------------------------------------------------------*) let gen_lemmas () = !system_gen_lemmas;; (*----------------------------------------------------------------------------*) (* max_var_depth : term -> int *) (* *) (* Returns the maximum depth of any variable in a term. *) (* eg. max_var_depth `PRE (a + SUC c)` = 4 *) (* max_var_depth `a` = 1 *) (* max_var_depth `PRE (5 + SUC 2)` = 0 *) (* max_var_depth `PRE (a + SUC 2)` = 3 *) (*----------------------------------------------------------------------------*) (* This is primarily used to limit non-termination. If max_var_depth exceeds *) (* a limit the system will fail. *) (* The algorithm is simple: *) (* if constant,numeral,etc then 0 *) (* else if variable then 1 *) (* else if definition,constructor,accessor then *) (* if (max_var_depth of arguments) > 0 then result + 1 *) (* else 0 *) (* else if any other combination then max_var_depth of arguments *) (*----------------------------------------------------------------------------*) let rec max_var_depth tm = if (is_var tm) then 1 else if ((is_numeral tm) or (is_const tm) or (is_T tm) or (is_F tm)) then 0 else try let (f,args) = strip_comb tm in let fn = (fst o dest_const) f in let l = flat [defs_names();all_constructors();all_accessors()] in if (mem fn l) then let x = itlist max (map max_var_depth args) 0 in if (x>0) then x+1 else 0 else itlist max (map max_var_depth args) 0 with Failure _ -> 0;;