skolem declarations for built-in theorems
authorpaulson
Tue Aug 08 18:40:56 2006 +0200 (2006-08-08)
changeset 20362bbff23c3e2ca
parent 20361 1aaf9ebe248d
child 20363 f34c5dbe74d5
skolem declarations for built-in theorems
src/HOL/Library/FuncSet.thy
src/HOL/Main.thy
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:20 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:56 2006 +0200
     1.3 @@ -219,4 +219,16 @@
     1.4          g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
     1.5    by (blast intro: card_inj order_antisym)
     1.6  
     1.7 +
     1.8 +(*The following declarations generate polymorphic Skolem functions for 
     1.9 +  these theorems. Eventually they should become redundant, once this 
    1.10 +  is done automatically.*)
    1.11 +
    1.12 +declare FuncSet.Pi_I [skolem]
    1.13 +declare FuncSet.Pi_mono [skolem]
    1.14 +declare FuncSet.extensionalityI [skolem]
    1.15 +declare FuncSet.funcsetI [skolem]
    1.16 +declare FuncSet.restrictI [skolem]
    1.17 +declare FuncSet.restrict_in_funcset [skolem]
    1.18 +
    1.19  end
     2.1 --- a/src/HOL/Main.thy	Tue Aug 08 18:40:20 2006 +0200
     2.2 +++ b/src/HOL/Main.thy	Tue Aug 08 18:40:56 2006 +0200
     2.3 @@ -19,4 +19,88 @@
     2.4  
     2.5  setup ResAxioms.setup
     2.6  
     2.7 +
     2.8 +(*The following declarations generate polymorphic Skolem functions for 
     2.9 +  these theorems. NOTE: We need an automatic mechanism to ensure that this
    2.10 +  happens for all theorems stored in descendant theories.*)
    2.11 +
    2.12 +(*HOL*)
    2.13 +declare ext [skolem]
    2.14 +
    2.15 +(*Finite_Set*)
    2.16 +declare setprod_nonneg [skolem]
    2.17 +declare setprod_pos [skolem]
    2.18 +declare setsum_bounded [skolem]
    2.19 +declare setsum_mono [skolem]
    2.20 +declare setsum_nonneg [skolem]
    2.21 +declare setsum_nonpos [skolem]
    2.22 +declare setsum_0' [skolem]
    2.23 +declare setprod_1' [skolem]
    2.24 +
    2.25 +declare Fun.image_INT [skolem]
    2.26 +
    2.27 +(*List. Only none look useful.*)
    2.28 +declare Cons_eq_append_conv [skolem]
    2.29 +declare Cons_eq_map_D [skolem]
    2.30 +declare Cons_eq_map_conv [skolem]
    2.31 +declare append_eq_Cons_conv [skolem]
    2.32 +declare map_eq_Cons_D [skolem]
    2.33 +declare map_eq_Cons_conv [skolem]
    2.34 +
    2.35 +declare Orderings.max_leastL [skolem]
    2.36 +declare Orderings.max_leastR [skolem]
    2.37 +
    2.38 +declare Product_Type.Sigma_mono [skolem]
    2.39 +
    2.40 +(*Relation*)
    2.41 +declare Domain_iff [skolem]
    2.42 +declare Image_iff [skolem]
    2.43 +declare Range_iff [skolem]
    2.44 +declare antisym_def [skolem]
    2.45 +declare reflI [skolem]
    2.46 +declare rel_compEpair [skolem]
    2.47 +declare refl_def [skolem]
    2.48 +declare sym_def [skolem]
    2.49 +declare trans_def [skolem]
    2.50 +declare single_valued_def [skolem]  
    2.51 +
    2.52 +(*Relation_Power*)
    2.53 +declare rel_pow_E2 [skolem]
    2.54 +declare rel_pow_E [skolem]
    2.55 +declare rel_pow_Suc_D2 [skolem]
    2.56 +declare rel_pow_Suc_D2' [skolem]
    2.57 +declare rel_pow_Suc_E [skolem]
    2.58 +
    2.59 +(*Set*)
    2.60 +declare Collect_mono [skolem]
    2.61 +declare INT_anti_mono [skolem]
    2.62 +declare INT_greatest [skolem]
    2.63 +declare INT_subset_iff [skolem]
    2.64 +declare Int_Collect_mono [skolem]
    2.65 +declare Inter_greatest[skolem]
    2.66 +declare UN_least [skolem]
    2.67 +declare UN_mono [skolem]
    2.68 +declare UN_subset_iff [skolem]
    2.69 +declare Union_least [skolem]
    2.70 +declare Union_disjoint [skolem]
    2.71 +declare disjoint_iff_not_equal [skolem]
    2.72 +declare image_subsetI [skolem]
    2.73 +declare image_subset_iff [skolem]
    2.74 +declare subset_def [skolem]
    2.75 +declare subset_iff [skolem]
    2.76 +
    2.77 +(*Transitive_Closure*)
    2.78 +declare converse_rtranclE [skolem]
    2.79 +declare irrefl_trancl_rD [skolem]
    2.80 +declare rtranclE [skolem]
    2.81 +declare tranclD [skolem]
    2.82 +declare tranclE [skolem]
    2.83 +
    2.84 +(*Wellfounded_Recursion*)
    2.85 +declare acyclicI [skolem]
    2.86 +declare acyclic_def [skolem]
    2.87 +declare wfI [skolem]
    2.88 +declare wf_def [skolem]
    2.89 +declare wf_eq_minimal [skolem]
    2.90 +
    2.91  end
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:20 2006 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:56 2006 +0200
     3.3 @@ -347,19 +347,12 @@
     3.4  
     3.5  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
     3.6  
     3.7 -(*These should include any plausibly-useful theorems, especially if they need
     3.8 -  Skolem functions. FIXME: this list is VERY INCOMPLETE*)
     3.9 -val default_initial_thms = map pairname
    3.10 -  [refl_def, antisym_def, sym_def, trans_def, single_valued_def,
    3.11 -   subset_refl, Union_least, Inter_greatest];
    3.12 -
    3.13  (*Setup function: takes a theory and installs ALL simprules and claset rules 
    3.14    into the clause cache*)
    3.15  fun clause_cache_setup thy =
    3.16    let val simps = simpset_rules_of_thy thy
    3.17        and clas  = claset_rules_of_thy thy
    3.18 -      and thy0  = List.foldl skolem_cache thy default_initial_thms
    3.19 -      val thy1  = List.foldl skolem_cache thy0 clas
    3.20 +      val thy1  = List.foldl skolem_cache thy clas
    3.21    in List.foldl skolem_cache thy1 simps end;
    3.22  (*Could be duplicate theorem names, due to multiple attributes*)
    3.23