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