src/HOL/Main.thy
author paulson
Tue Aug 08 18:40:56 2006 +0200 (2006-08-08)
changeset 20362 bbff23c3e2ca
parent 19608 81fe44909dd5
child 20414 029c4f9dc6f4
permissions -rw-r--r--
skolem declarations for built-in theorems
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports SAT Reconstruction ResAtpMethods
     9 begin
    10 
    11 text {*
    12   Theory @{text Main} includes everything.  Note that theory @{text
    13   PreList} already includes most HOL theories.
    14 *}
    15 
    16 text {* \medskip Late clause setup: installs \emph{all} simprules and
    17   claset rules into the clause cache; cf.\ theory @{text
    18   Reconstruction}. *}
    19 
    20 setup ResAxioms.setup
    21 
    22 
    23 (*The following declarations generate polymorphic Skolem functions for 
    24   these theorems. NOTE: We need an automatic mechanism to ensure that this
    25   happens for all theorems stored in descendant theories.*)
    26 
    27 (*HOL*)
    28 declare ext [skolem]
    29 
    30 (*Finite_Set*)
    31 declare setprod_nonneg [skolem]
    32 declare setprod_pos [skolem]
    33 declare setsum_bounded [skolem]
    34 declare setsum_mono [skolem]
    35 declare setsum_nonneg [skolem]
    36 declare setsum_nonpos [skolem]
    37 declare setsum_0' [skolem]
    38 declare setprod_1' [skolem]
    39 
    40 declare Fun.image_INT [skolem]
    41 
    42 (*List. Only none look useful.*)
    43 declare Cons_eq_append_conv [skolem]
    44 declare Cons_eq_map_D [skolem]
    45 declare Cons_eq_map_conv [skolem]
    46 declare append_eq_Cons_conv [skolem]
    47 declare map_eq_Cons_D [skolem]
    48 declare map_eq_Cons_conv [skolem]
    49 
    50 declare Orderings.max_leastL [skolem]
    51 declare Orderings.max_leastR [skolem]
    52 
    53 declare Product_Type.Sigma_mono [skolem]
    54 
    55 (*Relation*)
    56 declare Domain_iff [skolem]
    57 declare Image_iff [skolem]
    58 declare Range_iff [skolem]
    59 declare antisym_def [skolem]
    60 declare reflI [skolem]
    61 declare rel_compEpair [skolem]
    62 declare refl_def [skolem]
    63 declare sym_def [skolem]
    64 declare trans_def [skolem]
    65 declare single_valued_def [skolem]  
    66 
    67 (*Relation_Power*)
    68 declare rel_pow_E2 [skolem]
    69 declare rel_pow_E [skolem]
    70 declare rel_pow_Suc_D2 [skolem]
    71 declare rel_pow_Suc_D2' [skolem]
    72 declare rel_pow_Suc_E [skolem]
    73 
    74 (*Set*)
    75 declare Collect_mono [skolem]
    76 declare INT_anti_mono [skolem]
    77 declare INT_greatest [skolem]
    78 declare INT_subset_iff [skolem]
    79 declare Int_Collect_mono [skolem]
    80 declare Inter_greatest[skolem]
    81 declare UN_least [skolem]
    82 declare UN_mono [skolem]
    83 declare UN_subset_iff [skolem]
    84 declare Union_least [skolem]
    85 declare Union_disjoint [skolem]
    86 declare disjoint_iff_not_equal [skolem]
    87 declare image_subsetI [skolem]
    88 declare image_subset_iff [skolem]
    89 declare subset_def [skolem]
    90 declare subset_iff [skolem]
    91 
    92 (*Transitive_Closure*)
    93 declare converse_rtranclE [skolem]
    94 declare irrefl_trancl_rD [skolem]
    95 declare rtranclE [skolem]
    96 declare tranclD [skolem]
    97 declare tranclE [skolem]
    98 
    99 (*Wellfounded_Recursion*)
   100 declare acyclicI [skolem]
   101 declare acyclic_def [skolem]
   102 declare wfI [skolem]
   103 declare wf_def [skolem]
   104 declare wf_eq_minimal [skolem]
   105 
   106 end