HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue Sep 06 16:45:31 2011 +0900 (2011-09-06)
changeset 44740a2940bc24bad
parent 44730 11a1290fd0ac
child 44741 600d26952759
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/HOL4Compat.thy
     1.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Mon Sep 05 17:45:37 2011 -0700
     1.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Sep 06 16:45:31 2011 +0900
     1.3 @@ -12,17 +12,20 @@
     1.4  
     1.5  import_theory bool;
     1.6  
     1.7 +type_maps
     1.8 +  bool            > HOL.bool;
     1.9 +
    1.10  const_maps
    1.11 -  T               > True
    1.12 -  F               > False
    1.13 -  "!"             > All
    1.14 +  T               > HOL.True
    1.15 +  F               > HOL.False
    1.16 +  "!"             > HOL.All
    1.17    "/\\"           > HOL.conj
    1.18    "\\/"           > HOL.disj
    1.19 -  "?"             > Ex
    1.20 -  "?!"            > Ex1
    1.21 -  "~"             > Not
    1.22 +  "?"             > HOL.Ex
    1.23 +  "?!"            > HOL.Ex1
    1.24 +  "~"             > HOL.Not
    1.25    COND            > HOL.If
    1.26 -  bool_case       > Datatype.bool.bool_case
    1.27 +  bool_case       > Product_Type.bool.bool_case
    1.28    ONE_ONE         > HOL4Setup.ONE_ONE
    1.29    ONTO            > Fun.surj
    1.30    TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
    1.31 @@ -46,7 +49,7 @@
    1.32  import_theory sum;
    1.33  
    1.34  type_maps
    1.35 -  sum > "+";
    1.36 +  sum > Sum_Type.sum;
    1.37  
    1.38  const_maps
    1.39    INL      > Sum_Type.Inl
    1.40 @@ -55,7 +58,7 @@
    1.41    ISR      > HOL4Compat.ISR
    1.42    OUTL     > HOL4Compat.OUTL
    1.43    OUTR     > HOL4Compat.OUTR
    1.44 -  sum_case > Datatype.sum.sum_case;
    1.45 +  sum_case > Sum_Type.sum.sum_case;
    1.46  
    1.47  ignore_thms
    1.48    sum_TY_DEF
    1.49 @@ -63,7 +66,6 @@
    1.50    IS_SUM_REP
    1.51    INL_DEF
    1.52    INR_DEF
    1.53 -  sum_axiom
    1.54    sum_Axiom;
    1.55  
    1.56  end_import;
    1.57 @@ -125,13 +127,13 @@
    1.58      prod > Product_Type.prod;
    1.59  
    1.60  const_maps
    1.61 -    ","       > Pair
    1.62 -    FST       > fst
    1.63 -    SND       > snd
    1.64 -    CURRY     > curry
    1.65 -    UNCURRY   > split
    1.66 -    "##"      > map_pair
    1.67 -    pair_case > split;
    1.68 +    ","       > Product_Type.Pair
    1.69 +    FST       > Product_Type.fst
    1.70 +    SND       > Product_Type.snd
    1.71 +    CURRY     > Product_Type.curry
    1.72 +    UNCURRY   > Product_Type.prod.prod_case
    1.73 +    "##"      > Product_Type.map_pair
    1.74 +    pair_case > Product_Type.prod.prod_case;
    1.75  
    1.76  ignore_thms
    1.77      prod_TY_DEF
    1.78 @@ -145,11 +147,11 @@
    1.79  import_theory num;
    1.80  
    1.81  type_maps
    1.82 -  num > nat;
    1.83 +  num > Nat.nat;
    1.84  
    1.85  const_maps
    1.86 -  SUC > Suc
    1.87 -  0   > 0 :: nat;
    1.88 +  SUC > Nat.Suc
    1.89 +  0   > Groups.zero_class.zero :: nat;
    1.90  
    1.91  ignore_thms
    1.92      num_TY_DEF
    1.93 @@ -165,7 +167,7 @@
    1.94  import_theory prim_rec;
    1.95  
    1.96  const_maps
    1.97 -    "<" > Orderings.less :: "[nat,nat]=>bool";
    1.98 +    "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
    1.99  
   1.100  end_import;
   1.101  
   1.102 @@ -180,15 +182,15 @@
   1.103    ">"          > HOL4Compat.nat_gt
   1.104    ">="         > HOL4Compat.nat_ge
   1.105    FUNPOW       > HOL4Compat.FUNPOW
   1.106 -  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
   1.107 -  "+"          > Groups.plus :: "[nat,nat]=>nat"
   1.108 -  "*"          > Groups.times :: "[nat,nat]=>nat"
   1.109 -  "-"          > Groups.minus :: "[nat,nat]=>nat"
   1.110 -  MIN          > Orderings.min :: "[nat,nat]=>nat"
   1.111 -  MAX          > Orderings.max :: "[nat,nat]=>nat"
   1.112 -  DIV          > Divides.div :: "[nat,nat]=>nat"
   1.113 -  MOD          > Divides.mod :: "[nat,nat]=>nat"
   1.114 -  EXP          > Power.power :: "[nat,nat]=>nat";
   1.115 +  "<="         > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.116 +  "+"          > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.117 +  "*"          > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.118 +  "-"          > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.119 +  MIN          > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.120 +  MAX          > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.121 +  DIV          > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.122 +  MOD          > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.123 +  EXP          > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat";
   1.124  
   1.125  end_import;
   1.126  
   1.127 @@ -207,7 +209,7 @@
   1.128  import_theory divides;
   1.129  
   1.130  const_maps
   1.131 -  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
   1.132 +  divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
   1.133  
   1.134  end_import;
   1.135  
   1.136 @@ -227,7 +229,7 @@
   1.137    HD        > List.hd
   1.138    TL        > List.tl
   1.139    MAP       > List.map
   1.140 -  MEM       > "List.op mem"
   1.141 +  MEM       > HOL4Compat.list_mem
   1.142    FILTER    > List.filter
   1.143    FOLDL     > List.foldl
   1.144    EVERY     > List.list_all
   1.145 @@ -236,12 +238,12 @@
   1.146    FRONT     > List.butlast
   1.147    APPEND    > List.append
   1.148    FLAT      > List.concat
   1.149 -  LENGTH    > Nat.size
   1.150 +  LENGTH    > Nat.size_class.size
   1.151    REPLICATE > List.replicate
   1.152    list_size > HOL4Compat.list_size
   1.153    SUM       > HOL4Compat.sum
   1.154    FOLDR     > HOL4Compat.FOLDR
   1.155 -  EXISTS    > HOL4Compat.list_exists
   1.156 +  EXISTS    > List.list_ex
   1.157    MAP2      > HOL4Compat.map2
   1.158    ZIP       > HOL4Compat.ZIP
   1.159    UNZIP     > HOL4Compat.unzip;
     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Mon Sep 05 17:45:37 2011 -0700
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Tue Sep 06 16:45:31 2011 +0900
     2.3 @@ -16,13 +16,17 @@
     2.4    real > RealDef.real;
     2.5  
     2.6  const_maps
     2.7 -  real_0   > Groups.zero      :: real
     2.8 -  real_1   > Groups.one       :: real
     2.9 -  real_neg > Groups.uminus    :: "real => real"
    2.10 -  inv      > Groups.inverse   :: "real => real"
    2.11 -  real_add > Groups.plus      :: "[real,real] => real"
    2.12 -  real_mul > Groups.times     :: "[real,real] => real"
    2.13 -  real_lt  > Orderings.less      :: "[real,real] => bool";
    2.14 +  real_0   > Groups.zero_class.zero :: real
    2.15 +  real_1   > Groups.one_class.one   :: real
    2.16 +  real_neg > Groups.uminus_class.uminus :: "real \<Rightarrow> real"
    2.17 +  inv > Fields.inverse_class.inverse :: "real \<Rightarrow> real"
    2.18 +  real_add > Groups.plus_class.plus :: "real \<Rightarrow> real \<Rightarrow> real"
    2.19 +  real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
    2.20 +  real_mul > Groups.times_class.times :: "real \<Rightarrow> real \<Rightarrow> real"
    2.21 +  real_div > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
    2.22 +  real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
    2.23 +  mk_real > HOL.undefined   (* Otherwise proof_import_concl fails *)
    2.24 +  dest_real > HOL.undefined
    2.25  
    2.26  ignore_thms
    2.27      real_TY_DEF
    2.28 @@ -50,11 +54,11 @@
    2.29  const_maps
    2.30    real_gt     > HOL4Compat.real_gt
    2.31    real_ge     > HOL4Compat.real_ge
    2.32 -  real_lte    > Orderings.less_eq :: "[real,real] => bool"
    2.33 -  real_sub    > Groups.minus :: "[real,real] => real"
    2.34 -  "/"         > Fields.divide :: "[real,real] => real"
    2.35 -  pow         > Power.power :: "[real,nat] => real"
    2.36 -  abs         > Groups.abs :: "real => real"
    2.37 +  real_lte    > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
    2.38 +  real_sub    > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
    2.39 +  "/"         > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
    2.40 +  pow         > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
    2.41 +  abs         > Groups.abs_class.abs :: "real => real"
    2.42    real_of_num > RealDef.real :: "nat => real";
    2.43  
    2.44  end_import;
     3.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Sep 05 17:45:37 2011 -0700
     3.2 +++ b/src/HOL/Import/HOL4Compat.thy	Tue Sep 06 16:45:31 2011 +0900
     3.3 @@ -63,6 +63,14 @@
     3.4  lemma OUTR: "OUTR (Inr x) = x"
     3.5    by simp
     3.6  
     3.7 +lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
     3.8 +  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
     3.9 +  apply (simp_all add: o_def fun_eq_iff)
    3.10 +  apply (rule)
    3.11 +  apply (induct_tac x)
    3.12 +  apply simp_all
    3.13 +  done
    3.14 +
    3.15  lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
    3.16    by simp
    3.17  
    3.18 @@ -491,4 +499,6 @@
    3.19  lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
    3.20    by simp
    3.21  
    3.22 +definition [hol4rew]: "list_mem x xs = List.member xs x"
    3.23 +
    3.24  end