# HG changeset patch
# User paulson
# Date 1155055256 -7200
# Node ID bbff23c3e2caf7ec1d16f7c0391c29d1fc4746ab
# Parent  1aaf9ebe248d7f182ba426db7bbfedaad0c0b768
skolem declarations for built-in theorems

diff -r 1aaf9ebe248d -r bbff23c3e2ca src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:20 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:56 2006 +0200
@@ -219,4 +219,16 @@
         g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
   by (blast intro: card_inj order_antisym)
 
+
+(*The following declarations generate polymorphic Skolem functions for 
+  these theorems. Eventually they should become redundant, once this 
+  is done automatically.*)
+
+declare FuncSet.Pi_I [skolem]
+declare FuncSet.Pi_mono [skolem]
+declare FuncSet.extensionalityI [skolem]
+declare FuncSet.funcsetI [skolem]
+declare FuncSet.restrictI [skolem]
+declare FuncSet.restrict_in_funcset [skolem]
+
 end
diff -r 1aaf9ebe248d -r bbff23c3e2ca src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Aug 08 18:40:20 2006 +0200
+++ b/src/HOL/Main.thy	Tue Aug 08 18:40:56 2006 +0200
@@ -19,4 +19,88 @@
 
 setup ResAxioms.setup
 
+
+(*The following declarations generate polymorphic Skolem functions for 
+  these theorems. NOTE: We need an automatic mechanism to ensure that this
+  happens for all theorems stored in descendant theories.*)
+
+(*HOL*)
+declare ext [skolem]
+
+(*Finite_Set*)
+declare setprod_nonneg [skolem]
+declare setprod_pos [skolem]
+declare setsum_bounded [skolem]
+declare setsum_mono [skolem]
+declare setsum_nonneg [skolem]
+declare setsum_nonpos [skolem]
+declare setsum_0' [skolem]
+declare setprod_1' [skolem]
+
+declare Fun.image_INT [skolem]
+
+(*List. Only none look useful.*)
+declare Cons_eq_append_conv [skolem]
+declare Cons_eq_map_D [skolem]
+declare Cons_eq_map_conv [skolem]
+declare append_eq_Cons_conv [skolem]
+declare map_eq_Cons_D [skolem]
+declare map_eq_Cons_conv [skolem]
+
+declare Orderings.max_leastL [skolem]
+declare Orderings.max_leastR [skolem]
+
+declare Product_Type.Sigma_mono [skolem]
+
+(*Relation*)
+declare Domain_iff [skolem]
+declare Image_iff [skolem]
+declare Range_iff [skolem]
+declare antisym_def [skolem]
+declare reflI [skolem]
+declare rel_compEpair [skolem]
+declare refl_def [skolem]
+declare sym_def [skolem]
+declare trans_def [skolem]
+declare single_valued_def [skolem]  
+
+(*Relation_Power*)
+declare rel_pow_E2 [skolem]
+declare rel_pow_E [skolem]
+declare rel_pow_Suc_D2 [skolem]
+declare rel_pow_Suc_D2' [skolem]
+declare rel_pow_Suc_E [skolem]
+
+(*Set*)
+declare Collect_mono [skolem]
+declare INT_anti_mono [skolem]
+declare INT_greatest [skolem]
+declare INT_subset_iff [skolem]
+declare Int_Collect_mono [skolem]
+declare Inter_greatest[skolem]
+declare UN_least [skolem]
+declare UN_mono [skolem]
+declare UN_subset_iff [skolem]
+declare Union_least [skolem]
+declare Union_disjoint [skolem]
+declare disjoint_iff_not_equal [skolem]
+declare image_subsetI [skolem]
+declare image_subset_iff [skolem]
+declare subset_def [skolem]
+declare subset_iff [skolem]
+
+(*Transitive_Closure*)
+declare converse_rtranclE [skolem]
+declare irrefl_trancl_rD [skolem]
+declare rtranclE [skolem]
+declare tranclD [skolem]
+declare tranclE [skolem]
+
+(*Wellfounded_Recursion*)
+declare acyclicI [skolem]
+declare acyclic_def [skolem]
+declare wfI [skolem]
+declare wf_def [skolem]
+declare wf_eq_minimal [skolem]
+
 end
diff -r 1aaf9ebe248d -r bbff23c3e2ca src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:20 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:56 2006 +0200
@@ -347,19 +347,12 @@
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
-(*These should include any plausibly-useful theorems, especially if they need
-  Skolem functions. FIXME: this list is VERY INCOMPLETE*)
-val default_initial_thms = map pairname
-  [refl_def, antisym_def, sym_def, trans_def, single_valued_def,
-   subset_refl, Union_least, Inter_greatest];
-
 (*Setup function: takes a theory and installs ALL simprules and claset rules 
   into the clause cache*)
 fun clause_cache_setup thy =
   let val simps = simpset_rules_of_thy thy
       and clas  = claset_rules_of_thy thy
-      and thy0  = List.foldl skolem_cache thy default_initial_thms
-      val thy1  = List.foldl skolem_cache thy0 clas
+      val thy1  = List.foldl skolem_cache thy clas
   in List.foldl skolem_cache thy1 simps end;
 (*Could be duplicate theorem names, due to multiple attributes*)