src/HOL/Import/Generate-HOL/GenHOL4Base.thy

HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.

(*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
    Author:     Sebastian Skalberg, TU Muenchen
*)

theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;

import_segment "hol4";

setup_dump "../HOL" "HOL4Base";

append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};

import_theory bool;

type_maps
  bool            > HOL.bool;

const_maps
  T               > HOL.True
  F               > HOL.False
  "!"             > HOL.All
  "/\\"           > HOL.conj
  "\\/"           > HOL.disj
  "?"             > HOL.Ex
  "?!"            > HOL.Ex1
  "~"             > HOL.Not
  COND            > HOL.If
  bool_case       > Product_Type.bool.bool_case
  ONE_ONE         > HOL4Setup.ONE_ONE
  ONTO            > Fun.surj
  TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
  LET             > HOL4Compat.LET;

ignore_thms
  BOUNDED_DEF
  BOUNDED_THM
  UNBOUNDED_DEF
  UNBOUNDED_THM;

end_import;

import_theory combin;

const_maps
  o > Fun.comp;

end_import;

import_theory sum;

type_maps
  sum > Sum_Type.sum;

const_maps
  INL      > Sum_Type.Inl
  INR      > Sum_Type.Inr
  ISL      > HOL4Compat.ISL
  ISR      > HOL4Compat.ISR
  OUTL     > HOL4Compat.OUTL
  OUTR     > HOL4Compat.OUTR
  sum_case > Sum_Type.sum.sum_case;

ignore_thms
  sum_TY_DEF
  sum_ISO_DEF
  IS_SUM_REP
  INL_DEF
  INR_DEF
  sum_Axiom;

end_import;

import_theory one;

type_maps
  one > Product_Type.unit;

const_maps
  one > Product_Type.Unity;

ignore_thms
    one_TY_DEF
    one_axiom
    one_Axiom
    one_DEF;

end_import;

import_theory option;

type_maps
    option > Option.option;

const_maps
    NONE        > Option.option.None
    SOME        > Option.option.Some
    option_case > Option.option.option_case
    OPTION_MAP  > Option.map
    THE         > Option.the
    IS_SOME     > HOL4Compat.IS_SOME
    IS_NONE     > HOL4Compat.IS_NONE
    OPTION_JOIN > HOL4Compat.OPTION_JOIN;

ignore_thms
    option_axiom
    option_Axiom
    option_TY_DEF
    option_REP_ABS_DEF
    SOME_DEF
    NONE_DEF;

end_import;

import_theory marker;
end_import;

import_theory relation;

const_renames
  reflexive > pred_reflexive;

end_import;

import_theory pair;

type_maps
    prod > Product_Type.prod;

const_maps
    ","       > Product_Type.Pair
    FST       > Product_Type.fst
    SND       > Product_Type.snd
    CURRY     > Product_Type.curry
    UNCURRY   > Product_Type.prod.prod_case
    "##"      > Product_Type.map_pair
    pair_case > Product_Type.prod.prod_case;

ignore_thms
    prod_TY_DEF
    MK_PAIR_DEF
    IS_PAIR_DEF
    ABS_REP_prod
    COMMA_DEF;

end_import;

import_theory num;

type_maps
  num > Nat.nat;

const_maps
  SUC > Nat.Suc
  0   > Groups.zero_class.zero :: nat;

ignore_thms
    num_TY_DEF
    num_ISO_DEF
    IS_NUM_REP
    ZERO_REP_DEF
    SUC_REP_DEF
    ZERO_DEF
    SUC_DEF;

end_import;

import_theory prim_rec;

const_maps
    "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";

end_import;

import_theory arithmetic;

const_maps
  ALT_ZERO     > HOL4Compat.ALT_ZERO
  NUMERAL_BIT1 > HOL4Compat.NUMERAL_BIT1
  NUMERAL_BIT2 > HOL4Compat.NUMERAL_BIT2
  NUMERAL      > HOL4Compat.NUMERAL
  num_case     > Nat.nat.nat_case
  ">"          > HOL4Compat.nat_gt
  ">="         > HOL4Compat.nat_ge
  FUNPOW       > HOL4Compat.FUNPOW
  "<="         > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  "+"          > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  "*"          > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  "-"          > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  MIN          > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  MAX          > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  DIV          > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  MOD          > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  EXP          > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat";

end_import;

import_theory hrat;
end_import;

import_theory hreal;
end_import;

import_theory numeral;
end_import;

import_theory ind_type;
end_import;

import_theory divides;

const_maps
  divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";

end_import;

import_theory prime;
end_import;

import_theory list;

type_maps
    list > List.list;

const_maps
  CONS      > List.list.Cons
  NIL       > List.list.Nil
  list_case > List.list.list_case
  NULL      > List.null
  HD        > List.hd
  TL        > List.tl
  MAP       > List.map
  MEM       > HOL4Compat.list_mem
  FILTER    > List.filter
  FOLDL     > List.foldl
  EVERY     > List.list_all
  REVERSE   > List.rev
  LAST      > List.last
  FRONT     > List.butlast
  APPEND    > List.append
  FLAT      > List.concat
  LENGTH    > Nat.size_class.size
  REPLICATE > List.replicate
  list_size > HOL4Compat.list_size
  SUM       > HOL4Compat.sum
  FOLDR     > HOL4Compat.FOLDR
  EXISTS    > List.list_ex
  MAP2      > HOL4Compat.map2
  ZIP       > HOL4Compat.ZIP
  UNZIP     > HOL4Compat.unzip;

ignore_thms
  list_TY_DEF
  list_repfns
  list0_def
  list1_def
  NIL
  CONS_def;

end_import;

import_theory pred_set;
end_import;

import_theory operator;
end_import;

import_theory rich_list;
end_import;

import_theory state_transformer;
end_import;

append_dump "end";

flush_dump;

import_segment "";

end