src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
changeset 37540 48273d1ea331
parent 37518 efb0923cc098
child 37541 a76ace919f1c
equal deleted inserted replaced
37539:c80e77e8d036 37540:48273d1ea331
   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))