rename internal Sledgehammer constant
authorblanchet
Tue Sep 14 09:12:28 2010 +0200 (2010-09-14)
changeset 39355104a6d9e493e
parent 39354 cd20519eb9d0
child 39356 1ccc5c9ee343
rename internal Sledgehammer constant
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Sep 14 08:50:46 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Sep 14 09:12:28 2010 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     1.5  by simp
     1.6  
     1.7 -definition skolem_id :: "'a \<Rightarrow> 'a" where
     1.8 -[no_atp]: "skolem_id = (\<lambda>x. x)"
     1.9 +definition skolem :: "'a \<Rightarrow> 'a" where
    1.10 +[no_atp]: "skolem = (\<lambda>x. x)"
    1.11  
    1.12  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.13  [no_atp]: "COMBI P = P"
     2.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Sep 14 08:50:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Sep 14 09:12:28 2010 +0200
     2.3 @@ -40,9 +40,9 @@
     2.4  
     2.5  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
     2.6  
     2.7 -fun mk_skolem_id t =
     2.8 +fun mk_skolem t =
     2.9    let val T = fastype_of t in
    2.10 -    Const (@{const_name skolem_id}, T --> T) $ t
    2.11 +    Const (@{const_name skolem}, T --> T) $ t
    2.12    end
    2.13  
    2.14  fun beta_eta_under_lambdas (Abs (s, T, t')) =
    2.15 @@ -62,7 +62,7 @@
    2.16            val rhs =
    2.17              list_abs_free (map dest_Free args,
    2.18                             HOLogic.choice_const T $ beta_eta_under_lambdas body)
    2.19 -            |> mk_skolem_id
    2.20 +            |> mk_skolem
    2.21            val comb = list_comb (rhs, args)
    2.22          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    2.23        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    2.24 @@ -88,7 +88,7 @@
    2.25           $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
    2.26    | _ => th
    2.27  
    2.28 -fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
    2.29 +fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    2.30    | is_quasi_lambda_free (t1 $ t2) =
    2.31      is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    2.32    | is_quasi_lambda_free (Abs _) = false
    2.33 @@ -188,7 +188,7 @@
    2.34        in  c_variant_abs_multi (ct, cv::vars)  end
    2.35        handle CTERM _ => (ct0, rev vars);
    2.36  
    2.37 -val skolem_id_def_raw = @{thms skolem_id_def_raw}
    2.38 +val skolem_def_raw = @{thms skolem_def_raw}
    2.39  
    2.40  (* Given the definition of a Skolem function, return a theorem to replace
    2.41     an existential formula by a use of that function.
    2.42 @@ -209,8 +209,8 @@
    2.43        Drule.list_comb (rhs, frees)
    2.44        |> Drule.beta_conv cabs |> Thm.capply cTrueprop
    2.45      fun tacf [prem] =
    2.46 -      rewrite_goals_tac skolem_id_def_raw
    2.47 -      THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) RS @{thm someI_ex}) 1
    2.48 +      rewrite_goals_tac skolem_def_raw
    2.49 +      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
    2.50    in
    2.51      Goal.prove_internal [ex_tm] conc tacf
    2.52      |> forall_intr_list frees
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Sep 14 08:50:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Sep 14 09:12:28 2010 +0200
     3.3 @@ -443,10 +443,10 @@
     3.4    skolem_infix ^ "g"
     3.5  
     3.6  fun conceal_skolem_terms i skolems t =
     3.7 -  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
     3.8 +  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
     3.9      let
    3.10        fun aux skolems
    3.11 -              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
    3.12 +              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
    3.13            let
    3.14              val (skolems, s) =
    3.15                if i = ~1 then
    3.16 @@ -513,7 +513,7 @@
    3.17      fun aux (Const x) =
    3.18          fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
    3.19        | aux (Abs (_, _, u)) = aux u
    3.20 -      | aux (Const (@{const_name skolem_id}, _) $ _) = I
    3.21 +      | aux (Const (@{const_name skolem}, _) $ _) = I
    3.22        | aux (t $ u) = aux t #> aux u
    3.23        | aux _ = I
    3.24    in aux end