src/HOL/Import/HOL/transc.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "tdiv" > "tdiv_def"
     7   "tan" > "tan_def"
     8   "sqrt" > "sqrt_def"
     9   "sin" > "sin_def"
    10   "rsum" > "rsum_def"
    11   "root" > "root_def"
    12   "pi" > "pi_def"
    13   "ln" > "ln_def"
    14   "gauge" > "gauge_def"
    15   "fine" > "fine_def"
    16   "exp" > "exp_def"
    17   "dsize" > "dsize_def"
    18   "division" > "division_def"
    19   "cos" > "cos_def"
    20   "atn" > "atn_def"
    21   "asn" > "asn_def"
    22   "acs" > "acs_def"
    23   "Dint" > "Dint_def"
    24 
    25 const_maps
    26   "tdiv" > "HOL4Real.transc.tdiv"
    27   "tan" > "HOL4Real.transc.tan"
    28   "sqrt" > "HOL4Real.transc.sqrt"
    29   "sin" > "HOL4Real.transc.sin"
    30   "rsum" > "HOL4Real.transc.rsum"
    31   "root" > "HOL4Real.transc.root"
    32   "pi" > "HOL4Real.transc.pi"
    33   "ln" > "HOL4Real.transc.ln"
    34   "gauge" > "HOL4Real.transc.gauge"
    35   "fine" > "HOL4Real.transc.fine"
    36   "exp" > "HOL4Real.transc.exp"
    37   "dsize" > "HOL4Real.transc.dsize"
    38   "division" > "HOL4Real.transc.division"
    39   "cos" > "HOL4Real.transc.cos"
    40   "atn" > "HOL4Real.transc.atn"
    41   "asn" > "HOL4Real.transc.asn"
    42   "acs" > "HOL4Real.transc.acs"
    43   "Dint" > "HOL4Real.transc.Dint"
    44 
    45 thm_maps
    46   "tdiv_def" > "HOL4Real.transc.tdiv_def"
    47   "tdiv" > "HOL4Real.transc.tdiv"
    48   "tan_def" > "HOL4Real.transc.tan_def"
    49   "tan" > "HOL4Real.transc.tan"
    50   "sqrt_def" > "HOL4Real.transc.sqrt_def"
    51   "sqrt" > "HOL4Real.transc.sqrt"
    52   "sin_def" > "HOL4Real.transc.sin_def"
    53   "sin" > "HOL4Real.transc.sin"
    54   "rsum_def" > "HOL4Real.transc.rsum_def"
    55   "rsum" > "HOL4Real.transc.rsum"
    56   "root_def" > "HOL4Real.transc.root_def"
    57   "root" > "HOL4Real.transc.root"
    58   "pi_def" > "HOL4Real.transc.pi_def"
    59   "pi" > "HOL4Real.transc.pi"
    60   "ln_def" > "HOL4Real.transc.ln_def"
    61   "ln" > "HOL4Real.transc.ln"
    62   "gauge_def" > "HOL4Real.transc.gauge_def"
    63   "gauge" > "HOL4Real.transc.gauge"
    64   "fine_def" > "HOL4Real.transc.fine_def"
    65   "fine" > "HOL4Real.transc.fine"
    66   "exp_def" > "HOL4Real.transc.exp_def"
    67   "exp" > "HOL4Real.transc.exp"
    68   "dsize_def" > "HOL4Real.transc.dsize_def"
    69   "dsize" > "HOL4Real.transc.dsize"
    70   "division_def" > "HOL4Real.transc.division_def"
    71   "division" > "HOL4Real.transc.division"
    72   "cos_def" > "HOL4Real.transc.cos_def"
    73   "cos" > "HOL4Real.transc.cos"
    74   "atn_def" > "HOL4Real.transc.atn_def"
    75   "atn" > "HOL4Real.transc.atn"
    76   "asn_def" > "HOL4Real.transc.asn_def"
    77   "asn" > "HOL4Real.transc.asn"
    78   "acs_def" > "HOL4Real.transc.acs_def"
    79   "acs" > "HOL4Real.transc.acs"
    80   "TAN_TOTAL_POS" > "HOL4Real.transc.TAN_TOTAL_POS"
    81   "TAN_TOTAL_LEMMA" > "HOL4Real.transc.TAN_TOTAL_LEMMA"
    82   "TAN_TOTAL" > "HOL4Real.transc.TAN_TOTAL"
    83   "TAN_SEC" > "HOL4Real.transc.TAN_SEC"
    84   "TAN_POS_PI2" > "HOL4Real.transc.TAN_POS_PI2"
    85   "TAN_PI" > "HOL4Real.transc.TAN_PI"
    86   "TAN_PERIODIC" > "HOL4Real.transc.TAN_PERIODIC"
    87   "TAN_NPI" > "HOL4Real.transc.TAN_NPI"
    88   "TAN_NEG" > "HOL4Real.transc.TAN_NEG"
    89   "TAN_DOUBLE" > "HOL4Real.transc.TAN_DOUBLE"
    90   "TAN_ATN" > "HOL4Real.transc.TAN_ATN"
    91   "TAN_ADD" > "HOL4Real.transc.TAN_ADD"
    92   "TAN_0" > "HOL4Real.transc.TAN_0"
    93   "SQRT_POW_2" > "HOL4Real.transc.SQRT_POW_2"
    94   "SQRT_POW2" > "HOL4Real.transc.SQRT_POW2"
    95   "SQRT_POS_UNIQ" > "HOL4Real.transc.SQRT_POS_UNIQ"
    96   "SQRT_POS_LT" > "HOL4Real.transc.SQRT_POS_LT"
    97   "SQRT_POS_LE" > "HOL4Real.transc.SQRT_POS_LE"
    98   "SQRT_MUL" > "HOL4Real.transc.SQRT_MUL"
    99   "SQRT_MONO_LE" > "HOL4Real.transc.SQRT_MONO_LE"
   100   "SQRT_INV" > "HOL4Real.transc.SQRT_INV"
   101   "SQRT_EVEN_POW2" > "HOL4Real.transc.SQRT_EVEN_POW2"
   102   "SQRT_EQ" > "HOL4Real.transc.SQRT_EQ"
   103   "SQRT_DIV" > "HOL4Real.transc.SQRT_DIV"
   104   "SQRT_1" > "HOL4Real.transc.SQRT_1"
   105   "SQRT_0" > "HOL4Real.transc.SQRT_0"
   106   "SIN_ZERO_LEMMA" > "HOL4Real.transc.SIN_ZERO_LEMMA"
   107   "SIN_ZERO" > "HOL4Real.transc.SIN_ZERO"
   108   "SIN_TOTAL" > "HOL4Real.transc.SIN_TOTAL"
   109   "SIN_POS_PI_LE" > "HOL4Real.transc.SIN_POS_PI_LE"
   110   "SIN_POS_PI2_LE" > "HOL4Real.transc.SIN_POS_PI2_LE"
   111   "SIN_POS_PI2" > "HOL4Real.transc.SIN_POS_PI2"
   112   "SIN_POS_PI" > "HOL4Real.transc.SIN_POS_PI"
   113   "SIN_POS" > "HOL4Real.transc.SIN_POS"
   114   "SIN_PI2" > "HOL4Real.transc.SIN_PI2"
   115   "SIN_PI" > "HOL4Real.transc.SIN_PI"
   116   "SIN_PERIODIC_PI" > "HOL4Real.transc.SIN_PERIODIC_PI"
   117   "SIN_PERIODIC" > "HOL4Real.transc.SIN_PERIODIC"
   118   "SIN_PAIRED" > "HOL4Real.transc.SIN_PAIRED"
   119   "SIN_NPI" > "HOL4Real.transc.SIN_NPI"
   120   "SIN_NEGLEMMA" > "HOL4Real.transc.SIN_NEGLEMMA"
   121   "SIN_NEG" > "HOL4Real.transc.SIN_NEG"
   122   "SIN_FDIFF" > "HOL4Real.transc.SIN_FDIFF"
   123   "SIN_DOUBLE" > "HOL4Real.transc.SIN_DOUBLE"
   124   "SIN_COS_SQRT" > "HOL4Real.transc.SIN_COS_SQRT"
   125   "SIN_COS_SQ" > "HOL4Real.transc.SIN_COS_SQ"
   126   "SIN_COS_NEG" > "HOL4Real.transc.SIN_COS_NEG"
   127   "SIN_COS_ADD" > "HOL4Real.transc.SIN_COS_ADD"
   128   "SIN_COS" > "HOL4Real.transc.SIN_COS"
   129   "SIN_CONVERGES" > "HOL4Real.transc.SIN_CONVERGES"
   130   "SIN_CIRCLE" > "HOL4Real.transc.SIN_CIRCLE"
   131   "SIN_BOUNDS" > "HOL4Real.transc.SIN_BOUNDS"
   132   "SIN_BOUND" > "HOL4Real.transc.SIN_BOUND"
   133   "SIN_ASN" > "HOL4Real.transc.SIN_ASN"
   134   "SIN_ADD" > "HOL4Real.transc.SIN_ADD"
   135   "SIN_ACS_NZ" > "HOL4Real.transc.SIN_ACS_NZ"
   136   "SIN_0" > "HOL4Real.transc.SIN_0"
   137   "ROOT_POW_POS" > "HOL4Real.transc.ROOT_POW_POS"
   138   "ROOT_POS_UNIQ" > "HOL4Real.transc.ROOT_POS_UNIQ"
   139   "ROOT_POS_LT" > "HOL4Real.transc.ROOT_POS_LT"
   140   "ROOT_POS" > "HOL4Real.transc.ROOT_POS"
   141   "ROOT_MUL" > "HOL4Real.transc.ROOT_MUL"
   142   "ROOT_MONO_LE" > "HOL4Real.transc.ROOT_MONO_LE"
   143   "ROOT_LT_LEMMA" > "HOL4Real.transc.ROOT_LT_LEMMA"
   144   "ROOT_LN" > "HOL4Real.transc.ROOT_LN"
   145   "ROOT_INV" > "HOL4Real.transc.ROOT_INV"
   146   "ROOT_DIV" > "HOL4Real.transc.ROOT_DIV"
   147   "ROOT_1" > "HOL4Real.transc.ROOT_1"
   148   "ROOT_0" > "HOL4Real.transc.ROOT_0"
   149   "REAL_DIV_SQRT" > "HOL4Real.transc.REAL_DIV_SQRT"
   150   "POW_ROOT_POS" > "HOL4Real.transc.POW_ROOT_POS"
   151   "POW_2_SQRT" > "HOL4Real.transc.POW_2_SQRT"
   152   "PI_POS" > "HOL4Real.transc.PI_POS"
   153   "PI2_BOUNDS" > "HOL4Real.transc.PI2_BOUNDS"
   154   "PI2" > "HOL4Real.transc.PI2"
   155   "MCLAURIN_ZERO" > "HOL4Real.transc.MCLAURIN_ZERO"
   156   "MCLAURIN_NEG" > "HOL4Real.transc.MCLAURIN_NEG"
   157   "MCLAURIN_EXP_LT" > "HOL4Real.transc.MCLAURIN_EXP_LT"
   158   "MCLAURIN_EXP_LE" > "HOL4Real.transc.MCLAURIN_EXP_LE"
   159   "MCLAURIN_ALL_LT" > "HOL4Real.transc.MCLAURIN_ALL_LT"
   160   "MCLAURIN_ALL_LE" > "HOL4Real.transc.MCLAURIN_ALL_LE"
   161   "MCLAURIN" > "HOL4Real.transc.MCLAURIN"
   162   "LN_POW" > "HOL4Real.transc.LN_POW"
   163   "LN_POS" > "HOL4Real.transc.LN_POS"
   164   "LN_MUL" > "HOL4Real.transc.LN_MUL"
   165   "LN_MONO_LT" > "HOL4Real.transc.LN_MONO_LT"
   166   "LN_MONO_LE" > "HOL4Real.transc.LN_MONO_LE"
   167   "LN_LT_X" > "HOL4Real.transc.LN_LT_X"
   168   "LN_LE" > "HOL4Real.transc.LN_LE"
   169   "LN_INV" > "HOL4Real.transc.LN_INV"
   170   "LN_INJ" > "HOL4Real.transc.LN_INJ"
   171   "LN_EXP" > "HOL4Real.transc.LN_EXP"
   172   "LN_DIV" > "HOL4Real.transc.LN_DIV"
   173   "LN_1" > "HOL4Real.transc.LN_1"
   174   "INTEGRAL_NULL" > "HOL4Real.transc.INTEGRAL_NULL"
   175   "GAUGE_MIN" > "HOL4Real.transc.GAUGE_MIN"
   176   "FTC1" > "HOL4Real.transc.FTC1"
   177   "FINE_MIN" > "HOL4Real.transc.FINE_MIN"
   178   "EXP_TOTAL_LEMMA" > "HOL4Real.transc.EXP_TOTAL_LEMMA"
   179   "EXP_TOTAL" > "HOL4Real.transc.EXP_TOTAL"
   180   "EXP_SUB" > "HOL4Real.transc.EXP_SUB"
   181   "EXP_POS_LT" > "HOL4Real.transc.EXP_POS_LT"
   182   "EXP_POS_LE" > "HOL4Real.transc.EXP_POS_LE"
   183   "EXP_NZ" > "HOL4Real.transc.EXP_NZ"
   184   "EXP_NEG_MUL2" > "HOL4Real.transc.EXP_NEG_MUL2"
   185   "EXP_NEG_MUL" > "HOL4Real.transc.EXP_NEG_MUL"
   186   "EXP_NEG" > "HOL4Real.transc.EXP_NEG"
   187   "EXP_N" > "HOL4Real.transc.EXP_N"
   188   "EXP_MONO_LT" > "HOL4Real.transc.EXP_MONO_LT"
   189   "EXP_MONO_LE" > "HOL4Real.transc.EXP_MONO_LE"
   190   "EXP_MONO_IMP" > "HOL4Real.transc.EXP_MONO_IMP"
   191   "EXP_LT_1" > "HOL4Real.transc.EXP_LT_1"
   192   "EXP_LN" > "HOL4Real.transc.EXP_LN"
   193   "EXP_LE_X" > "HOL4Real.transc.EXP_LE_X"
   194   "EXP_INJ" > "HOL4Real.transc.EXP_INJ"
   195   "EXP_FDIFF" > "HOL4Real.transc.EXP_FDIFF"
   196   "EXP_CONVERGES" > "HOL4Real.transc.EXP_CONVERGES"
   197   "EXP_ADD_MUL" > "HOL4Real.transc.EXP_ADD_MUL"
   198   "EXP_ADD" > "HOL4Real.transc.EXP_ADD"
   199   "EXP_0" > "HOL4Real.transc.EXP_0"
   200   "Dint_def" > "HOL4Real.transc.Dint_def"
   201   "Dint" > "HOL4Real.transc.Dint"
   202   "DIVISION_UBOUND_LT" > "HOL4Real.transc.DIVISION_UBOUND_LT"
   203   "DIVISION_UBOUND" > "HOL4Real.transc.DIVISION_UBOUND"
   204   "DIVISION_THM" > "HOL4Real.transc.DIVISION_THM"
   205   "DIVISION_SINGLE" > "HOL4Real.transc.DIVISION_SINGLE"
   206   "DIVISION_RHS" > "HOL4Real.transc.DIVISION_RHS"
   207   "DIVISION_LT_GEN" > "HOL4Real.transc.DIVISION_LT_GEN"
   208   "DIVISION_LT" > "HOL4Real.transc.DIVISION_LT"
   209   "DIVISION_LHS" > "HOL4Real.transc.DIVISION_LHS"
   210   "DIVISION_LE" > "HOL4Real.transc.DIVISION_LE"
   211   "DIVISION_LBOUND_LT" > "HOL4Real.transc.DIVISION_LBOUND_LT"
   212   "DIVISION_LBOUND" > "HOL4Real.transc.DIVISION_LBOUND"
   213   "DIVISION_GT" > "HOL4Real.transc.DIVISION_GT"
   214   "DIVISION_EXISTS" > "HOL4Real.transc.DIVISION_EXISTS"
   215   "DIVISION_EQ" > "HOL4Real.transc.DIVISION_EQ"
   216   "DIVISION_APPEND" > "HOL4Real.transc.DIVISION_APPEND"
   217   "DIVISION_1" > "HOL4Real.transc.DIVISION_1"
   218   "DIVISION_0" > "HOL4Real.transc.DIVISION_0"
   219   "DINT_UNIQ" > "HOL4Real.transc.DINT_UNIQ"
   220   "DIFF_TAN" > "HOL4Real.transc.DIFF_TAN"
   221   "DIFF_SIN" > "HOL4Real.transc.DIFF_SIN"
   222   "DIFF_LN_COMPOSITE" > "HOL4Real.transc.DIFF_LN_COMPOSITE"
   223   "DIFF_LN" > "HOL4Real.transc.DIFF_LN"
   224   "DIFF_EXP" > "HOL4Real.transc.DIFF_EXP"
   225   "DIFF_COS" > "HOL4Real.transc.DIFF_COS"
   226   "DIFF_COMPOSITE" > "HOL4Real.transc.DIFF_COMPOSITE"
   227   "DIFF_ATN" > "HOL4Real.transc.DIFF_ATN"
   228   "DIFF_ASN_LEMMA" > "HOL4Real.transc.DIFF_ASN_LEMMA"
   229   "DIFF_ASN" > "HOL4Real.transc.DIFF_ASN"
   230   "DIFF_ACS_LEMMA" > "HOL4Real.transc.DIFF_ACS_LEMMA"
   231   "DIFF_ACS" > "HOL4Real.transc.DIFF_ACS"
   232   "COS_ZERO_LEMMA" > "HOL4Real.transc.COS_ZERO_LEMMA"
   233   "COS_ZERO" > "HOL4Real.transc.COS_ZERO"
   234   "COS_TOTAL" > "HOL4Real.transc.COS_TOTAL"
   235   "COS_SIN_SQRT" > "HOL4Real.transc.COS_SIN_SQRT"
   236   "COS_SIN_SQ" > "HOL4Real.transc.COS_SIN_SQ"
   237   "COS_SIN" > "HOL4Real.transc.COS_SIN"
   238   "COS_POS_PI_LE" > "HOL4Real.transc.COS_POS_PI_LE"
   239   "COS_POS_PI2_LE" > "HOL4Real.transc.COS_POS_PI2_LE"
   240   "COS_POS_PI2" > "HOL4Real.transc.COS_POS_PI2"
   241   "COS_POS_PI" > "HOL4Real.transc.COS_POS_PI"
   242   "COS_PI2" > "HOL4Real.transc.COS_PI2"
   243   "COS_PI" > "HOL4Real.transc.COS_PI"
   244   "COS_PERIODIC_PI" > "HOL4Real.transc.COS_PERIODIC_PI"
   245   "COS_PERIODIC" > "HOL4Real.transc.COS_PERIODIC"
   246   "COS_PAIRED" > "HOL4Real.transc.COS_PAIRED"
   247   "COS_NPI" > "HOL4Real.transc.COS_NPI"
   248   "COS_NEG" > "HOL4Real.transc.COS_NEG"
   249   "COS_ISZERO" > "HOL4Real.transc.COS_ISZERO"
   250   "COS_FDIFF" > "HOL4Real.transc.COS_FDIFF"
   251   "COS_DOUBLE" > "HOL4Real.transc.COS_DOUBLE"
   252   "COS_CONVERGES" > "HOL4Real.transc.COS_CONVERGES"
   253   "COS_BOUNDS" > "HOL4Real.transc.COS_BOUNDS"
   254   "COS_BOUND" > "HOL4Real.transc.COS_BOUND"
   255   "COS_ATN_NZ" > "HOL4Real.transc.COS_ATN_NZ"
   256   "COS_ASN_NZ" > "HOL4Real.transc.COS_ASN_NZ"
   257   "COS_ADD" > "HOL4Real.transc.COS_ADD"
   258   "COS_ACS" > "HOL4Real.transc.COS_ACS"
   259   "COS_2" > "HOL4Real.transc.COS_2"
   260   "COS_0" > "HOL4Real.transc.COS_0"
   261   "ATN_TAN" > "HOL4Real.transc.ATN_TAN"
   262   "ATN_BOUNDS" > "HOL4Real.transc.ATN_BOUNDS"
   263   "ATN" > "HOL4Real.transc.ATN"
   264   "ASN_SIN" > "HOL4Real.transc.ASN_SIN"
   265   "ASN_BOUNDS_LT" > "HOL4Real.transc.ASN_BOUNDS_LT"
   266   "ASN_BOUNDS" > "HOL4Real.transc.ASN_BOUNDS"
   267   "ASN" > "HOL4Real.transc.ASN"
   268   "ACS_COS" > "HOL4Real.transc.ACS_COS"
   269   "ACS_BOUNDS_LT" > "HOL4Real.transc.ACS_BOUNDS_LT"
   270   "ACS_BOUNDS" > "HOL4Real.transc.ACS_BOUNDS"
   271   "ACS" > "HOL4Real.transc.ACS"
   272 
   273 end