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