# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1315295131 -32400
# Node ID a2940bc24bad92ef1deeb09dda159004a45bd682
# Parent  11a1290fd0acff3e96887bb5ec0860bfc3d36418
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.

diff -r 11a1290fd0ac -r a2940bc24bad src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Sep 06 16:45:31 2011 +0900
@@ -12,17 +12,20 @@
 
 import_theory bool;
 
+type_maps
+  bool            > HOL.bool;
+
 const_maps
-  T               > True
-  F               > False
-  "!"             > All
+  T               > HOL.True
+  F               > HOL.False
+  "!"             > HOL.All
   "/\\"           > HOL.conj
   "\\/"           > HOL.disj
-  "?"             > Ex
-  "?!"            > Ex1
-  "~"             > Not
+  "?"             > HOL.Ex
+  "?!"            > HOL.Ex1
+  "~"             > HOL.Not
   COND            > HOL.If
-  bool_case       > Datatype.bool.bool_case
+  bool_case       > Product_Type.bool.bool_case
   ONE_ONE         > HOL4Setup.ONE_ONE
   ONTO            > Fun.surj
   TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
@@ -46,7 +49,7 @@
 import_theory sum;
 
 type_maps
-  sum > "+";
+  sum > Sum_Type.sum;
 
 const_maps
   INL      > Sum_Type.Inl
@@ -55,7 +58,7 @@
   ISR      > HOL4Compat.ISR
   OUTL     > HOL4Compat.OUTL
   OUTR     > HOL4Compat.OUTR
-  sum_case > Datatype.sum.sum_case;
+  sum_case > Sum_Type.sum.sum_case;
 
 ignore_thms
   sum_TY_DEF
@@ -63,7 +66,6 @@
   IS_SUM_REP
   INL_DEF
   INR_DEF
-  sum_axiom
   sum_Axiom;
 
 end_import;
@@ -125,13 +127,13 @@
     prod > Product_Type.prod;
 
 const_maps
-    ","       > Pair
-    FST       > fst
-    SND       > snd
-    CURRY     > curry
-    UNCURRY   > split
-    "##"      > map_pair
-    pair_case > split;
+    ","       > 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
@@ -145,11 +147,11 @@
 import_theory num;
 
 type_maps
-  num > nat;
+  num > Nat.nat;
 
 const_maps
-  SUC > Suc
-  0   > 0 :: nat;
+  SUC > Nat.Suc
+  0   > Groups.zero_class.zero :: nat;
 
 ignore_thms
     num_TY_DEF
@@ -165,7 +167,7 @@
 import_theory prim_rec;
 
 const_maps
-    "<" > Orderings.less :: "[nat,nat]=>bool";
+    "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
 
 end_import;
 
@@ -180,15 +182,15 @@
   ">"          > HOL4Compat.nat_gt
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
-  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
-  "+"          > Groups.plus :: "[nat,nat]=>nat"
-  "*"          > Groups.times :: "[nat,nat]=>nat"
-  "-"          > Groups.minus :: "[nat,nat]=>nat"
-  MIN          > Orderings.min :: "[nat,nat]=>nat"
-  MAX          > Orderings.max :: "[nat,nat]=>nat"
-  DIV          > Divides.div :: "[nat,nat]=>nat"
-  MOD          > Divides.mod :: "[nat,nat]=>nat"
-  EXP          > Power.power :: "[nat,nat]=>nat";
+  "<="         > 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;
 
@@ -207,7 +209,7 @@
 import_theory divides;
 
 const_maps
-  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
+  divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
 
 end_import;
 
@@ -227,7 +229,7 @@
   HD        > List.hd
   TL        > List.tl
   MAP       > List.map
-  MEM       > "List.op mem"
+  MEM       > HOL4Compat.list_mem
   FILTER    > List.filter
   FOLDL     > List.foldl
   EVERY     > List.list_all
@@ -236,12 +238,12 @@
   FRONT     > List.butlast
   APPEND    > List.append
   FLAT      > List.concat
-  LENGTH    > Nat.size
+  LENGTH    > Nat.size_class.size
   REPLICATE > List.replicate
   list_size > HOL4Compat.list_size
   SUM       > HOL4Compat.sum
   FOLDR     > HOL4Compat.FOLDR
-  EXISTS    > HOL4Compat.list_exists
+  EXISTS    > List.list_ex
   MAP2      > HOL4Compat.map2
   ZIP       > HOL4Compat.ZIP
   UNZIP     > HOL4Compat.unzip;
diff -r 11a1290fd0ac -r a2940bc24bad src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Tue Sep 06 16:45:31 2011 +0900
@@ -16,13 +16,17 @@
   real > RealDef.real;
 
 const_maps
-  real_0   > Groups.zero      :: real
-  real_1   > Groups.one       :: real
-  real_neg > Groups.uminus    :: "real => real"
-  inv      > Groups.inverse   :: "real => real"
-  real_add > Groups.plus      :: "[real,real] => real"
-  real_mul > Groups.times     :: "[real,real] => real"
-  real_lt  > Orderings.less      :: "[real,real] => bool";
+  real_0   > Groups.zero_class.zero :: real
+  real_1   > Groups.one_class.one   :: real
+  real_neg > Groups.uminus_class.uminus :: "real \<Rightarrow> real"
+  inv > Fields.inverse_class.inverse :: "real \<Rightarrow> real"
+  real_add > Groups.plus_class.plus :: "real \<Rightarrow> real \<Rightarrow> real"
+  real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
+  real_mul > Groups.times_class.times :: "real \<Rightarrow> real \<Rightarrow> real"
+  real_div > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
+  real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
+  mk_real > HOL.undefined   (* Otherwise proof_import_concl fails *)
+  dest_real > HOL.undefined
 
 ignore_thms
     real_TY_DEF
@@ -50,11 +54,11 @@
 const_maps
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
-  real_lte    > Orderings.less_eq :: "[real,real] => bool"
-  real_sub    > Groups.minus :: "[real,real] => real"
-  "/"         > Fields.divide :: "[real,real] => real"
-  pow         > Power.power :: "[real,nat] => real"
-  abs         > Groups.abs :: "real => real"
+  real_lte    > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
+  real_sub    > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
+  "/"         > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
+  pow         > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
+  abs         > Groups.abs_class.abs :: "real => real"
   real_of_num > RealDef.real :: "nat => real";
 
 end_import;
diff -r 11a1290fd0ac -r a2940bc24bad src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/HOL/Import/HOL4Compat.thy	Tue Sep 06 16:45:31 2011 +0900
@@ -63,6 +63,14 @@
 lemma OUTR: "OUTR (Inr x) = x"
   by simp
 
+lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
+  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
+  apply (simp_all add: o_def fun_eq_iff)
+  apply (rule)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
 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)"
   by simp
 
@@ -491,4 +499,6 @@
 lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
   by simp
 
+definition [hol4rew]: "list_mem x xs = List.member xs x"
+
 end