181 |
181 |
182 (*Returns the vars of a theorem*) |
182 (*Returns the vars of a theorem*) |
183 fun vars_of_thm th = |
183 fun vars_of_thm th = |
184 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
184 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
185 |
185 |
186 (*Make a version of fun_cong with a given variable name*) |
186 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} |
187 local |
187 |
188 val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
188 (* Removes the lambdas from an equation of the form t = (%x. u). *) |
189 val cx = hd (vars_of_thm fun_cong'); |
189 fun extensionalize th = |
190 val ty = typ_of (ctyp_of_term cx); |
190 case prop_of th of |
191 val thy = theory_of_thm fun_cong; |
191 _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) |
192 fun mkvar a = cterm_of thy (Var((a,0),ty)); |
192 $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) |
193 in |
193 | _ => th |
194 fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' |
|
195 end; |
|
196 |
|
197 (*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n, |
|
198 serves as an upper bound on how many to remove.*) |
|
199 fun strip_lambdas 0 th = th |
|
200 | strip_lambdas n th = |
|
201 case prop_of th of |
|
202 _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) => |
|
203 strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) |
|
204 | _ => th; |
|
205 |
194 |
206 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
195 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
207 | is_quasi_lambda_free (t1 $ t2) = |
196 | is_quasi_lambda_free (t1 $ t2) = |
208 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
197 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
209 | is_quasi_lambda_free (Abs _) = false |
198 | is_quasi_lambda_free (Abs _) = false |
337 |
326 |
338 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) |
327 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) |
339 fun to_nnf th ctxt0 = |
328 fun to_nnf th ctxt0 = |
340 let val th1 = th |> transform_elim |> zero_var_indexes |
329 let val th1 = th |> transform_elim |> zero_var_indexes |
341 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
330 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
342 val th3 = th2 |
331 val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize |
343 |> Conv.fconv_rule Object_Logic.atomize |
332 |> extensionalize |
344 |> Meson.make_nnf ctxt |> strip_lambdas ~1 |
333 |> Meson.make_nnf ctxt |
345 in (th3, ctxt) end; |
334 in (th3, ctxt) end; |
346 |
335 |
347 (*Generate Skolem functions for a theorem supplied in nnf*) |
336 (*Generate Skolem functions for a theorem supplied in nnf*) |
348 fun skolem_theorems_of_assume s th = |
337 fun skolem_theorems_of_assume s th = |
349 map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th)) |
338 map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th)) |