src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
author krauss
Fri Sep 09 00:22:18 2011 +0200 (2011-09-09)
changeset 44845 5e51075cbd97
parent 44064 5bce8ff0d9ae
child 44860 56101fa00193
permissions -rw-r--r--
added syntactic classes for "inf" and "sup"
obua@17322
     1
(*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
wenzelm@41589
     2
    Author:     Steven Obua, TU Muenchen
kaliszyk@43785
     3
    Author:     Cezary Kaliszyk
obua@17322
     4
*)
obua@17322
     5
kaliszyk@43785
     6
theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
obua@17322
     7
kaliszyk@43785
     8
;import_segment "hollight"
obua@19064
     9
kaliszyk@43785
    10
;setup_dump "../HOLLight" "HOLLight";
obua@17322
    11
kaliszyk@43785
    12
;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *}
obua@17322
    13
kaliszyk@43785
    14
;import_theory hollight
obua@17322
    15
kaliszyk@43785
    16
;ignore_thms
kaliszyk@43785
    17
  (* Unit type *)
kaliszyk@43785
    18
  TYDEF_1 DEF_one
kaliszyk@43785
    19
  (* Product type *)
kaliszyk@43785
    20
  TYDEF_prod "DEF_," DEF_mk_pair REP_ABS_PAIR
kaliszyk@43785
    21
  (* Option type *)
kaliszyk@43785
    22
  TYDEF_option DEF_NONE DEF_SOME
kaliszyk@43785
    23
  (* Sum type *)
kaliszyk@43785
    24
  TYDEF_sum DEF_INL DEF_INR DEF_OUTL DEF_OUTR
kaliszyk@43785
    25
  (* Naturals *)
kaliszyk@43785
    26
  TYDEF_num DEF__0 DEF_SUC
kaliszyk@43785
    27
  (* Lists *)
kaliszyk@43785
    28
  TYDEF_list DEF_NIL DEF_CONS DEF_HD DEF_TL DEF_MAP2 DEF_ITLIST2 ALL_MAP EX_MAP
kaliszyk@43785
    29
  DEF_ASSOC MEM_ASSOC DEF_ZIP EL_TL
obua@17322
    30
kaliszyk@43785
    31
  (* list_of_set uses Isabelle lists with HOLLight CARD *)
kaliszyk@43785
    32
  DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
kaliszyk@43843
    33
  MEM_LIST_OF_SET HAS_SIZE_SET_OF_LIST FINITE_SET_OF_LIST
kaliszyk@43785
    34
  (* UNIV *)
kaliszyk@43843
    35
  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM FSTCART_PASTECART
kaliszyk@43843
    36
  SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
kaliszyk@43785
    37
  (* Reals *)
kaliszyk@43785
    38
  (* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
kaliszyk@43785
    39
  DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
kaliszyk@43785
    40
  (* Integers *)
kaliszyk@43785
    41
  (* TYDEF_int DEF_int_divides DEF_int_coprime*)
kaliszyk@43843
    42
  (* HOLLight CARD and CASEWISE with Isabelle lists *)
kaliszyk@43843
    43
  CARD_SET_OF_LIST_LE CASEWISE CASEWISE_CASES RECURSION_CASEWISE CASEWISE_WORKS
kaliszyk@43843
    44
  WF_REC_CASES RECURSION_CASEWISE_PAIRWISE
kaliszyk@43785
    45
kaliszyk@43785
    46
;type_maps
kaliszyk@43785
    47
  bool > HOL.bool
kaliszyk@43785
    48
  "fun" > "fun"
obua@17322
    49
  N_1 >  Product_Type.unit
haftmann@37678
    50
  prod > Product_Type.prod
kaliszyk@43785
    51
  ind > Nat.ind
haftmann@37391
    52
  num > Nat.nat
haftmann@37678
    53
  sum > Sum_Type.sum
kaliszyk@43785
    54
  option > Datatype.option
kaliszyk@43785
    55
  list > List.list
kaliszyk@43785
    56
(*real > RealDef.real *)
kaliszyk@43785
    57
(*int > Int.int *)
obua@17322
    58
kaliszyk@43785
    59
;const_renames
obua@17444
    60
  "==" > "eqeq"
kaliszyk@43785
    61
  "ALL" > list_ALL
kaliszyk@43785
    62
  "EX" > list_EX
obua@17444
    63
kaliszyk@43785
    64
;const_maps
kaliszyk@43785
    65
  T > HOL.True
kaliszyk@43785
    66
  F > HOL.False
haftmann@38864
    67
  "=" > HOL.eq
haftmann@38786
    68
  "==>" > HOL.implies
haftmann@38795
    69
  "/\\" > HOL.conj
haftmann@38795
    70
  "\\/" > HOL.disj
kaliszyk@43785
    71
  "!" > HOL.All
kaliszyk@43785
    72
  "?" > HOL.Ex
kaliszyk@43785
    73
  "?!" > HOL.Ex1
kaliszyk@43785
    74
  "~" > HOL.Not
kaliszyk@43785
    75
  COND > HOL.If
kaliszyk@43785
    76
  ONE_ONE > Fun.inj
kaliszyk@43785
    77
  ONTO > Fun.surj
obua@17322
    78
  o > Fun.comp
kaliszyk@43785
    79
  "@" > Hilbert_Choice.Eps
kaliszyk@43785
    80
  CHOICE > Hilbert_Choice.Eps
obua@17322
    81
  I > Fun.id
obua@17322
    82
  one > Product_Type.Unity
kaliszyk@43785
    83
  LET > HOLLightCompat.LET
obua@17322
    84
  mk_pair > Product_Type.Pair_Rep
kaliszyk@43785
    85
  "," > Product_Type.Pair
kaliszyk@43785
    86
  FST > Product_Type.fst
kaliszyk@43785
    87
  SND > Product_Type.snd
kaliszyk@43785
    88
  CURRY > Product_Type.curry
kaliszyk@43785
    89
  "_0" > Groups.zero_class.zero :: nat
kaliszyk@43785
    90
  SUC > Nat.Suc
obua@17322
    91
  PRE > HOLLightCompat.Pred
kaliszyk@43785
    92
  NUMERAL > HOLLightCompat.NUMERAL
kaliszyk@43785
    93
  mk_num > Fun.id
kaliszyk@43785
    94
  "+" > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
    95
  "*" > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
    96
  "-" > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
    97
  "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool"
kaliszyk@43785
    98
  "<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
kaliszyk@43785
    99
  ">" > Orderings.ord_class.greater :: "nat \<Rightarrow> nat \<Rightarrow> bool"
kaliszyk@43785
   100
  ">=" > Orderings.ord_class.greater_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
kaliszyk@43785
   101
  EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
   102
  MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
   103
  MIN > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
   104
  DIV > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
kaliszyk@43785
   105
  MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
obua@17322
   106
  BIT0 > HOLLightCompat.NUMERAL_BIT0
kaliszyk@43785
   107
  BIT1 > HOLLightCompat.NUMERAL_BIT1
obua@19064
   108
  INL > Sum_Type.Inl
obua@20326
   109
  INR > Sum_Type.Inr
kaliszyk@43785
   110
  OUTL > HOLLightCompat.OUTL
kaliszyk@43785
   111
  OUTR > HOLLightCompat.OUTR
kaliszyk@43785
   112
  NONE > Datatype.None
kaliszyk@43785
   113
  SOME > Datatype.Some
kaliszyk@43785
   114
  EVEN > Parity.even_odd_class.even :: "nat \<Rightarrow> bool"
kaliszyk@43785
   115
  ODD > HOLLightCompat.ODD
kaliszyk@43785
   116
  FACT > Fact.fact_class.fact :: "nat \<Rightarrow> nat"
kaliszyk@43785
   117
  WF > Wellfounded.wfP
kaliszyk@43785
   118
  NIL > List.list.Nil
kaliszyk@43785
   119
  CONS > List.list.Cons
kaliszyk@43785
   120
  APPEND > List.append
kaliszyk@43785
   121
  REVERSE > List.rev
kaliszyk@43785
   122
  LENGTH > List.length
kaliszyk@43785
   123
  MAP > List.map
kaliszyk@43785
   124
  LAST > List.last
kaliszyk@43785
   125
  BUTLAST > List.butlast
kaliszyk@43785
   126
  REPLICATE > List.replicate
kaliszyk@43785
   127
  ITLIST > List.foldr
kaliszyk@43785
   128
  list_ALL > List.list_all
kaliszyk@43785
   129
  ALL2 > List.list_all2
kaliszyk@43785
   130
  list_EX > List.list_ex
kaliszyk@43785
   131
  FILTER > List.filter
kaliszyk@43785
   132
  NULL > List.null
kaliszyk@43785
   133
  HD > List.hd
kaliszyk@43785
   134
  TL > List.tl
kaliszyk@43785
   135
  EL > HOLLightList.list_el
kaliszyk@43785
   136
  ZIP > List.zip
kaliszyk@43785
   137
  MAP2 > HOLLightList.map2
kaliszyk@43785
   138
  ITLIST2 > HOLLightList.fold2
kaliszyk@43785
   139
  MEM > HOLLightList.list_mem
kaliszyk@43785
   140
  set_of_list > List.set
kaliszyk@43785
   141
  IN > Set.member
kaliszyk@43785
   142
  INSERT > Set.insert
kaliszyk@43785
   143
  EMPTY > Orderings.bot_class.bot :: "'a \<Rightarrow> bool"
kaliszyk@43785
   144
  GABS > Hilbert_Choice.Eps
kaliszyk@43785
   145
  GEQ > HOL.eq
kaliszyk@43785
   146
  GSPEC > Set.Collect
kaliszyk@43785
   147
  SETSPEC > HOLLightCompat.SETSPEC
krauss@44845
   148
  UNION > Lattices.sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
kaliszyk@43785
   149
  UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
krauss@44845
   150
  INTER > Lattices.inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
kaliszyk@43785
   151
  INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
kaliszyk@43785
   152
  DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
kaliszyk@43785
   153
  SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
kaliszyk@43785
   154
  PSUBSET > Orderings.ord_class.less :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
kaliszyk@43785
   155
  DELETE > HOLLightCompat.DELETE
kaliszyk@43785
   156
  DISJOINT > HOLLightCompat.DISJOINT
kaliszyk@43785
   157
  IMAGE > Set.image
kaliszyk@43785
   158
  FINITE > Finite_Set.finite
kaliszyk@43785
   159
  INFINITE > HOLLightCompat.INFINITE
kaliszyk@43785
   160
  ".." > HOLLightCompat.dotdot
kaliszyk@43785
   161
  UNIV > Orderings.top_class.top :: "'a \<Rightarrow> bool"
kaliszyk@43785
   162
  MEASURE > HOLLightCompat.MEASURE
kaliszyk@43785
   163
(*real_of_num > RealDef.real :: "nat => real"
kaliszyk@43785
   164
  real_neg > Groups.uminus_class.uminus :: "real => real"
huffman@44064
   165
  real_inv > Fields.inverse_class.inverse :: "real => real"
kaliszyk@43785
   166
  real_add > Groups.plus_class.plus :: "real => real => real"
kaliszyk@43785
   167
  real_sub > Groups.minus_class.minus :: "real => real => real"
kaliszyk@43785
   168
  real_mul > Groups.times_class.times :: "real => real => real"
huffman@44064
   169
  real_div > Fields.inverse_class.divide :: "real => real => real"
kaliszyk@43785
   170
  real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
kaliszyk@43785
   171
  real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
kaliszyk@43785
   172
  real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
kaliszyk@43785
   173
  real_ge > Orderings.ord_class.greater_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
kaliszyk@43785
   174
  real_pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
kaliszyk@43785
   175
  real_abs > Groups.abs_class.abs :: "real \<Rightarrow> real"
kaliszyk@43785
   176
  real_max > Orderings.ord_class.max :: "real \<Rightarrow> real \<Rightarrow> real"
kaliszyk@43785
   177
  real_min > Orderings.ord_class.min :: "real \<Rightarrow> real \<Rightarrow> real"
kaliszyk@43785
   178
  real_sgn > Groups.sgn_class.sgn :: "real \<Rightarrow> real"*)
kaliszyk@43785
   179
(*real_of_int > RealDef.real :: "int => real"
kaliszyk@43785
   180
  int_of_real > Archimedean_Field.floor :: "real \<Rightarrow> int"
kaliszyk@43785
   181
  dest_int > RealDef.real :: "int => real"
kaliszyk@43785
   182
  mk_int > Archimedean_Field.floor :: "real \<Rightarrow> int"
kaliszyk@43785
   183
  int_lt > Orderings.ord_class.less :: "int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   184
  int_le > Orderings.ord_class.less_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   185
  int_gt > Orderings.ord_class.greater :: "int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   186
  int_ge > Orderings.ord_class.greater_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   187
  int_of_num > Nat.semiring_1_class.of_nat :: "nat \<Rightarrow> int"
kaliszyk@43785
   188
  int_neg > Groups.uminus_class.uminus :: "int \<Rightarrow> int"
kaliszyk@43785
   189
  int_add > Groups.plus_class.plus :: "int => int => int"
kaliszyk@43785
   190
  int_sub > Groups.minus_class.minus :: "int => int => int"
kaliszyk@43785
   191
  int_mul > Groups.times_class.times :: "int => int => int"
kaliszyk@43785
   192
  int_abs > Groups.abs_class.abs :: "int \<Rightarrow> int"
kaliszyk@43785
   193
  int_max > Orderings.ord_class.max :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   194
  int_min > Orderings.ord_class.min :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   195
  int_sgn > Groups.sgn_class.sgn :: "int \<Rightarrow> int"
kaliszyk@43785
   196
  int_pow > Power.power_class.power :: "int \<Rightarrow> nat \<Rightarrow> int"
kaliszyk@43785
   197
  int_div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   198
  div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   199
  mod_int > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   200
  rem > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
kaliszyk@43785
   201
  int_divides > Rings.dvd_class.dvd :: "int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   202
  int_mod > HOLLightInt.int_mod :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
kaliszyk@43785
   203
  int_gcd > HOLLightInt.int_gcd :: "int \<times> int \<Rightarrow> int"
kaliszyk@43785
   204
  int_coprime > HOLLightInt.int_coprime :: "int \<times> int \<Rightarrow> bool"
kaliszyk@43785
   205
  eqeq > HOLLightInt.eqeq*)
obua@17440
   206
kaliszyk@43785
   207
;end_import
obua@17322
   208
kaliszyk@43785
   209
;append_dump "end"
obua@17322
   210
kaliszyk@43785
   211
;flush_dump
obua@17322
   212
kaliszyk@43785
   213
;import_segment ""
obua@17322
   214
obua@17322
   215
end