src/HOL/Main.thy
changeset 20362 bbff23c3e2ca
parent 19608 81fe44909dd5
child 20414 029c4f9dc6f4
     1.1 --- a/src/HOL/Main.thy	Tue Aug 08 18:40:20 2006 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Aug 08 18:40:56 2006 +0200
     1.3 @@ -19,4 +19,88 @@
     1.4  
     1.5  setup ResAxioms.setup
     1.6  
     1.7 +
     1.8 +(*The following declarations generate polymorphic Skolem functions for 
     1.9 +  these theorems. NOTE: We need an automatic mechanism to ensure that this
    1.10 +  happens for all theorems stored in descendant theories.*)
    1.11 +
    1.12 +(*HOL*)
    1.13 +declare ext [skolem]
    1.14 +
    1.15 +(*Finite_Set*)
    1.16 +declare setprod_nonneg [skolem]
    1.17 +declare setprod_pos [skolem]
    1.18 +declare setsum_bounded [skolem]
    1.19 +declare setsum_mono [skolem]
    1.20 +declare setsum_nonneg [skolem]
    1.21 +declare setsum_nonpos [skolem]
    1.22 +declare setsum_0' [skolem]
    1.23 +declare setprod_1' [skolem]
    1.24 +
    1.25 +declare Fun.image_INT [skolem]
    1.26 +
    1.27 +(*List. Only none look useful.*)
    1.28 +declare Cons_eq_append_conv [skolem]
    1.29 +declare Cons_eq_map_D [skolem]
    1.30 +declare Cons_eq_map_conv [skolem]
    1.31 +declare append_eq_Cons_conv [skolem]
    1.32 +declare map_eq_Cons_D [skolem]
    1.33 +declare map_eq_Cons_conv [skolem]
    1.34 +
    1.35 +declare Orderings.max_leastL [skolem]
    1.36 +declare Orderings.max_leastR [skolem]
    1.37 +
    1.38 +declare Product_Type.Sigma_mono [skolem]
    1.39 +
    1.40 +(*Relation*)
    1.41 +declare Domain_iff [skolem]
    1.42 +declare Image_iff [skolem]
    1.43 +declare Range_iff [skolem]
    1.44 +declare antisym_def [skolem]
    1.45 +declare reflI [skolem]
    1.46 +declare rel_compEpair [skolem]
    1.47 +declare refl_def [skolem]
    1.48 +declare sym_def [skolem]
    1.49 +declare trans_def [skolem]
    1.50 +declare single_valued_def [skolem]  
    1.51 +
    1.52 +(*Relation_Power*)
    1.53 +declare rel_pow_E2 [skolem]
    1.54 +declare rel_pow_E [skolem]
    1.55 +declare rel_pow_Suc_D2 [skolem]
    1.56 +declare rel_pow_Suc_D2' [skolem]
    1.57 +declare rel_pow_Suc_E [skolem]
    1.58 +
    1.59 +(*Set*)
    1.60 +declare Collect_mono [skolem]
    1.61 +declare INT_anti_mono [skolem]
    1.62 +declare INT_greatest [skolem]
    1.63 +declare INT_subset_iff [skolem]
    1.64 +declare Int_Collect_mono [skolem]
    1.65 +declare Inter_greatest[skolem]
    1.66 +declare UN_least [skolem]
    1.67 +declare UN_mono [skolem]
    1.68 +declare UN_subset_iff [skolem]
    1.69 +declare Union_least [skolem]
    1.70 +declare Union_disjoint [skolem]
    1.71 +declare disjoint_iff_not_equal [skolem]
    1.72 +declare image_subsetI [skolem]
    1.73 +declare image_subset_iff [skolem]
    1.74 +declare subset_def [skolem]
    1.75 +declare subset_iff [skolem]
    1.76 +
    1.77 +(*Transitive_Closure*)
    1.78 +declare converse_rtranclE [skolem]
    1.79 +declare irrefl_trancl_rD [skolem]
    1.80 +declare rtranclE [skolem]
    1.81 +declare tranclD [skolem]
    1.82 +declare tranclE [skolem]
    1.83 +
    1.84 +(*Wellfounded_Recursion*)
    1.85 +declare acyclicI [skolem]
    1.86 +declare acyclic_def [skolem]
    1.87 +declare wfI [skolem]
    1.88 +declare wf_def [skolem]
    1.89 +declare wf_eq_minimal [skolem]
    1.90 +
    1.91  end