1 (******************************************************************************)
2 (* FILE : environment.ml *)
3 (* DESCRIPTION : Environment of definitions and pre-proved theorems for use *)
6 (* READS FILES : <none> *)
7 (* WRITES FILES : <none> *)
9 (* AUTHOR : R.J.Boulton *)
10 (* DATE : 8th May 1991 *)
12 (* LAST MODIFIED : R.J.Boulton *)
13 (* DATE : 12th October 1992 *)
15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
16 (* DATE : July 2009 *)
17 (******************************************************************************)
19 let my_gen_terms = ref ([]:term list);;
20 let bm_steps = ref (0,0);;
24 let wl,w = dest_thm th in
26 GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th)
29 let LIST_CONJ = end_itlist CONJ ;;
31 let rec CONJ_LIST n th =
32 try if n=1 then [th] else (CONJUNCT1 th)::(CONJ_LIST (n-1) (CONJUNCT2 th))
33 with Failure _ -> failwith "CONJ_LIST";;
35 (*----------------------------------------------------------------------------*)
36 (* Reference variable to hold the defining theorems for operators currently *)
37 (* defined within the system. Each definition is stored as a triple. The *)
38 (* first component is the name of the operator. The second is the number of *)
39 (* the recursive argument. If the operator is not defined recursively, this *)
40 (* number is zero. The third component is a list of pairs of type constructor *)
41 (* names and the theorems that define the behaviour of the operator for each *)
42 (* constructor. If the operator is not recursive, the constructor names are *)
43 (* empty (null) strings. *)
44 (*----------------------------------------------------------------------------*)
46 let system_defs = ref ([] : (string * (int * (string * thm) list)) list);;
48 (*----------------------------------------------------------------------------*)
49 (* new_def : thm -> void *)
51 (* Make a new definition available. Checks that theorem has no hypotheses, *)
52 (* then splits it into conjuncts. The variables for each conjunct are *)
53 (* specialised and then the conjuncts are made into equations. *)
55 (* For each equation, a triple is obtained, consisting of the name of the *)
56 (* function on the LHS, the number of the recursive argument, and the name of *)
57 (* the constructor used in that argument. This process fails if the LHS is *)
58 (* not an application of a constant (possibly to zero arguments), or if more *)
59 (* than one of the arguments is anything other than a variable. The argument *)
60 (* that is not a variable must be an application of a constructor. If the *)
61 (* function is not recursive, the argument number returned is zero. *)
63 (* Having obtained a triple for each equation, a check is made that the first *)
64 (* two components are the same for each equation. Then, the equations are *)
65 (* saved together with constructor names for each, and the name of the *)
66 (* operator being defined, and the number of the recursive argument. *)
67 (*----------------------------------------------------------------------------*)
71 (let make_into_eqn th =
73 in if (is_eq tm) then th
74 else if (is_neg tm) then EQF_INTRO th
76 and get_constructor th =
77 let tm = lhs (concl th)
78 in let (f,args) = strip_comb tm
79 in let name = fst (dest_const f)
80 in let bools = number_list (map is_var args)
81 in let i = itlist (fun (b,i) n -> if ((not b) & (n = 0)) then i
82 else if b then n else failwith "") bools 0
85 else ((name,i),fst (dest_const (fst (strip_comb (el (i-1) args)))))
86 in let ([],tm) = dest_thm th
87 in let ths = CONJ_LIST (length (conj_list tm)) th
88 in let ths' = map SPEC_ALL ths
89 in let eqs = map make_into_eqn ths'
90 in let constructs = map get_constructor eqs
91 in let (xl,yl) = hashI setify (List.split constructs)
92 in let (name,i) = if (length xl = 1) then (hd xl) else failwith ""
93 in system_defs := (name,(i,List.combine yl eqs))::(!system_defs)
94 ) with Failure _ -> failwith "new_def";;
96 (*----------------------------------------------------------------------------*)
97 (* defs : void -> thm list list *)
99 (* Returns a list of lists of theorems currently being used as definitions. *)
100 (* Each list in the list is for one operator. *)
101 (*----------------------------------------------------------------------------*)
103 let defs () = map ((map snd) o snd o snd) (!system_defs);;
104 let defs_names () = map fst (!system_defs);;
106 (*----------------------------------------------------------------------------*)
107 (* get_def : string -> (string # int # (string # thm) list) *)
109 (* Function to obtain the definition information of a named operator. *)
110 (*----------------------------------------------------------------------------*)
112 let get_def name = try ( assoc name (!system_defs) ) with Failure _ -> failwith "get_def";;
114 (*----------------------------------------------------------------------------*)
115 (* Reference variable for a list of theorems currently proved in the system. *)
116 (* These theorems are available to the automatic proof procedures for use as *)
117 (* rewrite rules. The elements of the list are actually pairs of theorems. *)
118 (* The first theorem is that specified by the user. The second is an *)
119 (* equivalent theorem in a standard form. *)
120 (*----------------------------------------------------------------------------*)
122 let system_rewrites = ref ([] : (thm * thm) list);;
124 (*----------------------------------------------------------------------------*)
125 (* CONJ_IMP_IMP_IMP = |- x /\ y ==> z = x ==> y ==> z *)
126 (*----------------------------------------------------------------------------*)
128 let CONJ_IMP_IMP_IMP =
130 (`((x /\ y) ==> z) = (x ==> (y ==> z))`,
131 BOOL_CASES_TAC `x:bool` THEN
132 BOOL_CASES_TAC `y:bool` THEN
133 BOOL_CASES_TAC `z:bool` THEN
136 (*----------------------------------------------------------------------------*)
137 (* CONJ_UNDISCH : thm -> thm *)
139 (* Undischarges the conjuncts of the antecedant of an implication. *)
140 (* e.g. |- x /\ (y /\ z) /\ w ==> x ---> x, y /\ z, w |- x *)
142 (* Has to check for negations, because UNDISCH processes them when we don't *)
144 (*----------------------------------------------------------------------------*)
146 let rec CONJ_UNDISCH th =
148 (let th' = CONV_RULE (REWR_CONV CONJ_IMP_IMP_IMP) th
149 in let th'' = UNDISCH th'
150 in CONJ_UNDISCH th'')
151 with Failure _ -> try (if not (is_neg (concl th)) then UNDISCH th else failwith "")
152 with Failure _ -> failwith "CONJ_UNDISCH";;
154 (*----------------------------------------------------------------------------*)
155 (* new_rewrite_rule : thm -> void *)
157 (* Make a new rewrite rule available. Checks that theorem has no hypotheses. *)
158 (* The theorem is saved together with an equivalent theorem in a standard *)
159 (* form. Theorems are fully generalized, then specialized with unique *)
160 (* variable names (genvars), and then standardized as follows: *)
162 (* |- (h1 /\ ... /\ hn) ==> (l = r) ---> h1, ..., hn |- l = r *)
163 (* |- (h1 /\ ... /\ hn) ==> ~b ---> h1, ..., hn |- b = F *)
164 (* |- (h1 /\ ... /\ hn) ==> b ---> h1, ..., hn |- b = T *)
165 (* |- l = r ---> |- l = r *)
166 (* |- ~b ---> |- b = F *)
167 (* |- b ---> |- b = T *)
169 (* A conjunction of rules may be given. The function will treat each conjunct *)
170 (* in the theorem as a separate rule. *)
171 (*----------------------------------------------------------------------------*)
173 let rec new_rewrite_rule th =
174 try (if (is_conj (concl th))
175 then (map new_rewrite_rule (CONJUNCTS th); ())
176 else let ([],tm) = dest_thm th
177 in let th' = GSPEC (GEN_ALL th)
178 in let th'' = try (CONJ_UNDISCH th') with Failure _ -> th'
179 in let tm'' = concl th''
181 (if (is_eq tm'') then th''
182 else if (is_neg tm'') then EQF_INTRO th''
184 in system_rewrites := (th,th''')::(!system_rewrites)
185 ) with Failure _ -> failwith "new_rewrite_rule";;
187 (*----------------------------------------------------------------------------*)
188 (* rewrite_rules : void -> thm list *)
190 (* Returns the list of theorems currently being used as rewrites, in the form *)
191 (* they were originally given by the user. *)
192 (*----------------------------------------------------------------------------*)
194 let rewrite_rules () = map fst (!system_rewrites);;
196 (*----------------------------------------------------------------------------*)
197 (* Reference variable to hold the generalisation lemmas currently known to *)
199 (*----------------------------------------------------------------------------*)
201 let system_gen_lemmas = ref ([] : thm list);;
203 (*----------------------------------------------------------------------------*)
204 (* new_gen_lemma : thm -> void *)
206 (* Make a new generalisation lemma available. *)
207 (* Checks that the theorem has no hypotheses. *)
208 (*----------------------------------------------------------------------------*)
210 let new_gen_lemma th =
212 then system_gen_lemmas := th::(!system_gen_lemmas)
213 else failwith "new_gen_lemma";;
215 (*----------------------------------------------------------------------------*)
216 (* gen_lemmas : void -> thm list *)
218 (* Returns the list of theorems currently being used as *)
219 (* generalisation lemmas. *)
220 (*----------------------------------------------------------------------------*)
222 let gen_lemmas () = !system_gen_lemmas;;
226 (*----------------------------------------------------------------------------*)
227 (* max_var_depth : term -> int *)
229 (* Returns the maximum depth of any variable in a term. *)
230 (* eg. max_var_depth `PRE (a + SUC c)` = 4 *)
231 (* max_var_depth `a` = 1 *)
232 (* max_var_depth `PRE (5 + SUC 2)` = 0 *)
233 (* max_var_depth `PRE (a + SUC 2)` = 3 *)
234 (*----------------------------------------------------------------------------*)
235 (* This is primarily used to limit non-termination. If max_var_depth exceeds *)
236 (* a limit the system will fail. *)
237 (* The algorithm is simple: *)
238 (* if constant,numeral,etc then 0 *)
239 (* else if variable then 1 *)
240 (* else if definition,constructor,accessor then *)
241 (* if (max_var_depth of arguments) > 0 then result + 1 *)
243 (* else if any other combination then max_var_depth of arguments *)
244 (*----------------------------------------------------------------------------*)
247 let rec max_var_depth tm =
248 if (is_var tm) then 1
249 else if ((is_numeral tm)
251 or (is_T tm) or (is_F tm)) then 0
253 let (f,args) = strip_comb tm in
254 let fn = (fst o dest_const) f in
255 let l = flat [defs_names();all_constructors();all_accessors()] in
257 let x = itlist max (map max_var_depth args) 0 in
258 if (x>0) then x+1 else 0
259 else itlist max (map max_var_depth args) 0
260 with Failure _ -> 0;;