author blanchet Tue Sep 14 09:12:28 2010 +0200 (2010-09-14) changeset 39355 104a6d9e493e parent 39354 cd20519eb9d0 child 39356 1ccc5c9ee343
rename internal Sledgehammer constant
```     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
```