HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jul 13 00:23:24 2011 +0900 (2011-07-13)
changeset 437852bd54d4b5f3d
parent 43766 9545bb3cefac
child 43786 fea3ed6951e3
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLightInt.thy
src/HOL/Import/HOLLightList.thy
src/HOL/Import/HOLLightReal.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
     1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Wed Jul 13 00:23:24 2011 +0900
     1.3 @@ -1,104 +1,212 @@
     1.4  (*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
     1.5      Author:     Steven Obua, TU Muenchen
     1.6 +    Author:     Cezary Kaliszyk
     1.7  *)
     1.8  
     1.9 -theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
    1.10 +theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
    1.11  
    1.12 -(*;skip_import_dir "/home/obua/tmp/cache"
    1.13 -
    1.14 -;skip_import on*)
    1.15 +;import_segment "hollight"
    1.16  
    1.17 -;import_segment "hollight";
    1.18 -
    1.19 -setup_dump "../HOLLight" "HOLLight";
    1.20 +;setup_dump "../HOLLight" "HOLLight";
    1.21  
    1.22 -append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
    1.23 +;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *}
    1.24  
    1.25 -;import_theory hollight;
    1.26 +;import_theory hollight
    1.27  
    1.28 -ignore_thms
    1.29 -  TYDEF_1
    1.30 -  DEF_one
    1.31 -  TYDEF_prod
    1.32 -  TYDEF_num
    1.33 -  IND_SUC_0_EXISTS
    1.34 -  DEF__0
    1.35 -  DEF_SUC
    1.36 -  DEF_IND_SUC
    1.37 -  DEF_IND_0
    1.38 -  DEF_NUM_REP
    1.39 -  TYDEF_sum
    1.40 -  DEF_INL
    1.41 -  DEF_INR
    1.42 - (* TYDEF_option*);
    1.43 +;ignore_thms
    1.44 +  (* Unit type *)
    1.45 +  TYDEF_1 DEF_one
    1.46 +  (* Product type *)
    1.47 +  TYDEF_prod "DEF_," DEF_mk_pair REP_ABS_PAIR
    1.48 +  (* Option type *)
    1.49 +  TYDEF_option DEF_NONE DEF_SOME
    1.50 +  (* Sum type *)
    1.51 +  TYDEF_sum DEF_INL DEF_INR DEF_OUTL DEF_OUTR
    1.52 +  (* Naturals *)
    1.53 +  TYDEF_num DEF__0 DEF_SUC
    1.54 +  (* Lists *)
    1.55 +  TYDEF_list DEF_NIL DEF_CONS DEF_HD DEF_TL DEF_MAP2 DEF_ITLIST2 ALL_MAP EX_MAP
    1.56 +  DEF_ASSOC MEM_ASSOC DEF_ZIP EL_TL
    1.57  
    1.58 -type_maps
    1.59 -  ind > Nat.ind
    1.60 -  bool > bool
    1.61 -  fun > fun
    1.62 +  (* list_of_set uses Isabelle lists with HOLLight CARD *)
    1.63 +  DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
    1.64 +  MEM_LIST_OF_SET FINITE_SET_OF_LIST
    1.65 +  (* UNIV *)
    1.66 +  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM
    1.67 +  FSTCART_PASTECART SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
    1.68 +  (* Reals *)
    1.69 +  (* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
    1.70 +  DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
    1.71 +  (* Integers *)
    1.72 +  (* TYDEF_int DEF_int_divides DEF_int_coprime*)
    1.73 +
    1.74 +;type_maps
    1.75 +  bool > HOL.bool
    1.76 +  "fun" > "fun"
    1.77    N_1 >  Product_Type.unit
    1.78    prod > Product_Type.prod
    1.79 +  ind > Nat.ind
    1.80    num > Nat.nat
    1.81    sum > Sum_Type.sum
    1.82 -(*  option > Datatype.option*);
    1.83 +  option > Datatype.option
    1.84 +  list > List.list
    1.85 +(*real > RealDef.real *)
    1.86 +(*int > Int.int *)
    1.87  
    1.88 -const_renames
    1.89 +;const_renames
    1.90    "==" > "eqeq"
    1.91 -  ".." > "dotdot"
    1.92 -  "ALL" > ALL_list;
    1.93 +  "ALL" > list_ALL
    1.94 +  "EX" > list_EX
    1.95  
    1.96 -const_maps
    1.97 -  T > True
    1.98 -  F > False
    1.99 -  ONE_ONE > HOL4Setup.ONE_ONE
   1.100 -  ONTO    > Fun.surj
   1.101 +;const_maps
   1.102 +  T > HOL.True
   1.103 +  F > HOL.False
   1.104    "=" > HOL.eq
   1.105    "==>" > HOL.implies
   1.106    "/\\" > HOL.conj
   1.107    "\\/" > HOL.disj
   1.108 -  "!" > All
   1.109 -  "?" > Ex
   1.110 -  "?!" > Ex1
   1.111 -  "~" > Not
   1.112 +  "!" > HOL.All
   1.113 +  "?" > HOL.Ex
   1.114 +  "?!" > HOL.Ex1
   1.115 +  "~" > HOL.Not
   1.116 +  COND > HOL.If
   1.117 +  ONE_ONE > Fun.inj
   1.118 +  ONTO > Fun.surj
   1.119    o > Fun.comp
   1.120 -  "@" > "Hilbert_Choice.Eps"
   1.121 +  "@" > Hilbert_Choice.Eps
   1.122 +  CHOICE > Hilbert_Choice.Eps
   1.123    I > Fun.id
   1.124    one > Product_Type.Unity
   1.125 -  LET > HOL4Compat.LET
   1.126 +  LET > HOLLightCompat.LET
   1.127    mk_pair > Product_Type.Pair_Rep
   1.128 -  "," > Pair
   1.129 -  REP_prod > Rep_Prod
   1.130 -  ABS_prod > Abs_Prod
   1.131 -  FST > fst
   1.132 -  SND > snd
   1.133 -  "_0" > 0 :: nat
   1.134 -  SUC > Suc
   1.135 +  "," > Product_Type.Pair
   1.136 +  FST > Product_Type.fst
   1.137 +  SND > Product_Type.snd
   1.138 +  CURRY > Product_Type.curry
   1.139 +  "_0" > Groups.zero_class.zero :: nat
   1.140 +  SUC > Nat.Suc
   1.141    PRE > HOLLightCompat.Pred
   1.142 -  NUMERAL > HOL4Compat.NUMERAL
   1.143 -  "+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
   1.144 -  "*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.145 -  "-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.146 +  NUMERAL > HOLLightCompat.NUMERAL
   1.147 +  mk_num > Fun.id
   1.148 +  "+" > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.149 +  "*" > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.150 +  "-" > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.151 +  "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.152 +  "<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.153 +  ">" > Orderings.ord_class.greater :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.154 +  ">=" > Orderings.ord_class.greater_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   1.155 +  EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.156 +  MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.157 +  MIN > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.158 +  DIV > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.159 +  MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.160    BIT0 > HOLLightCompat.NUMERAL_BIT0
   1.161 -  BIT1 > HOL4Compat.NUMERAL_BIT1
   1.162 +  BIT1 > HOLLightCompat.NUMERAL_BIT1
   1.163    INL > Sum_Type.Inl
   1.164    INR > Sum_Type.Inr
   1.165 - (* NONE > Datatype.None
   1.166 -  SOME > Datatype.Some;
   1.167 -  HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
   1.168 -
   1.169 -(*import_until "TYDEF_sum"
   1.170 -
   1.171 -consts
   1.172 -print_theorems
   1.173 +  OUTL > HOLLightCompat.OUTL
   1.174 +  OUTR > HOLLightCompat.OUTR
   1.175 +  NONE > Datatype.None
   1.176 +  SOME > Datatype.Some
   1.177 +  EVEN > Parity.even_odd_class.even :: "nat \<Rightarrow> bool"
   1.178 +  ODD > HOLLightCompat.ODD
   1.179 +  FACT > Fact.fact_class.fact :: "nat \<Rightarrow> nat"
   1.180 +  WF > Wellfounded.wfP
   1.181 +  NIL > List.list.Nil
   1.182 +  CONS > List.list.Cons
   1.183 +  APPEND > List.append
   1.184 +  REVERSE > List.rev
   1.185 +  LENGTH > List.length
   1.186 +  MAP > List.map
   1.187 +  LAST > List.last
   1.188 +  BUTLAST > List.butlast
   1.189 +  REPLICATE > List.replicate
   1.190 +  ITLIST > List.foldr
   1.191 +  list_ALL > List.list_all
   1.192 +  ALL2 > List.list_all2
   1.193 +  list_EX > List.list_ex
   1.194 +  FILTER > List.filter
   1.195 +  NULL > List.null
   1.196 +  HD > List.hd
   1.197 +  TL > List.tl
   1.198 +  EL > HOLLightList.list_el
   1.199 +  ZIP > List.zip
   1.200 +  MAP2 > HOLLightList.map2
   1.201 +  ITLIST2 > HOLLightList.fold2
   1.202 +  MEM > HOLLightList.list_mem
   1.203 +  set_of_list > List.set
   1.204 +  IN > Set.member
   1.205 +  INSERT > Set.insert
   1.206 +  EMPTY > Orderings.bot_class.bot :: "'a \<Rightarrow> bool"
   1.207 +  GABS > Hilbert_Choice.Eps
   1.208 +  GEQ > HOL.eq
   1.209 +  GSPEC > Set.Collect
   1.210 +  SETSPEC > HOLLightCompat.SETSPEC
   1.211 +  UNION > Lattices.semilattice_sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.212 +  UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.213 +  INTER > Lattices.semilattice_inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.214 +  INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.215 +  DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.216 +  SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.217 +  PSUBSET > Orderings.ord_class.less :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.218 +  DELETE > HOLLightCompat.DELETE
   1.219 +  DISJOINT > HOLLightCompat.DISJOINT
   1.220 +  IMAGE > Set.image
   1.221 +  FINITE > Finite_Set.finite
   1.222 +  INFINITE > HOLLightCompat.INFINITE
   1.223 +  ".." > HOLLightCompat.dotdot
   1.224 +  UNIV > Orderings.top_class.top :: "'a \<Rightarrow> bool"
   1.225 +  MEASURE > HOLLightCompat.MEASURE
   1.226 +(*real_of_num > RealDef.real :: "nat => real"
   1.227 +  real_neg > Groups.uminus_class.uminus :: "real => real"
   1.228 +  real_inv > Rings.inverse_class.inverse :: "real => real"
   1.229 +  real_add > Groups.plus_class.plus :: "real => real => real"
   1.230 +  real_sub > Groups.minus_class.minus :: "real => real => real"
   1.231 +  real_mul > Groups.times_class.times :: "real => real => real"
   1.232 +  real_div > Rings.inverse_class.divide :: "real => real => real"
   1.233 +  real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
   1.234 +  real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
   1.235 +  real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
   1.236 +  real_ge > Orderings.ord_class.greater_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
   1.237 +  real_pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
   1.238 +  real_abs > Groups.abs_class.abs :: "real \<Rightarrow> real"
   1.239 +  real_max > Orderings.ord_class.max :: "real \<Rightarrow> real \<Rightarrow> real"
   1.240 +  real_min > Orderings.ord_class.min :: "real \<Rightarrow> real \<Rightarrow> real"
   1.241 +  real_sgn > Groups.sgn_class.sgn :: "real \<Rightarrow> real"*)
   1.242 +(*real_of_int > RealDef.real :: "int => real"
   1.243 +  int_of_real > Archimedean_Field.floor :: "real \<Rightarrow> int"
   1.244 +  dest_int > RealDef.real :: "int => real"
   1.245 +  mk_int > Archimedean_Field.floor :: "real \<Rightarrow> int"
   1.246 +  int_lt > Orderings.ord_class.less :: "int \<Rightarrow> int \<Rightarrow> bool"
   1.247 +  int_le > Orderings.ord_class.less_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
   1.248 +  int_gt > Orderings.ord_class.greater :: "int \<Rightarrow> int \<Rightarrow> bool"
   1.249 +  int_ge > Orderings.ord_class.greater_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
   1.250 +  int_of_num > Nat.semiring_1_class.of_nat :: "nat \<Rightarrow> int"
   1.251 +  int_neg > Groups.uminus_class.uminus :: "int \<Rightarrow> int"
   1.252 +  int_add > Groups.plus_class.plus :: "int => int => int"
   1.253 +  int_sub > Groups.minus_class.minus :: "int => int => int"
   1.254 +  int_mul > Groups.times_class.times :: "int => int => int"
   1.255 +  int_abs > Groups.abs_class.abs :: "int \<Rightarrow> int"
   1.256 +  int_max > Orderings.ord_class.max :: "int \<Rightarrow> int \<Rightarrow> int"
   1.257 +  int_min > Orderings.ord_class.min :: "int \<Rightarrow> int \<Rightarrow> int"
   1.258 +  int_sgn > Groups.sgn_class.sgn :: "int \<Rightarrow> int"
   1.259 +  int_pow > Power.power_class.power :: "int \<Rightarrow> nat \<Rightarrow> int"
   1.260 +  int_div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
   1.261 +  div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
   1.262 +  mod_int > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
   1.263 +  rem > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
   1.264 +  int_divides > Rings.dvd_class.dvd :: "int \<Rightarrow> int \<Rightarrow> bool"
   1.265 +  int_mod > HOLLightInt.int_mod :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
   1.266 +  int_gcd > HOLLightInt.int_gcd :: "int \<times> int \<Rightarrow> int"
   1.267 +  int_coprime > HOLLightInt.int_coprime :: "int \<times> int \<Rightarrow> bool"
   1.268 +  eqeq > HOLLightInt.eqeq*)
   1.269  
   1.270 -import_until *)
   1.271 +;end_import
   1.272  
   1.273 -end_import;
   1.274 +;append_dump "end"
   1.275  
   1.276 -append_dump "end";
   1.277 +;flush_dump
   1.278  
   1.279 -flush_dump;
   1.280 -
   1.281 -import_segment "";
   1.282 +;import_segment ""
   1.283  
   1.284  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Import/HOLLightInt.thy	Wed Jul 13 00:23:24 2011 +0900
     2.3 @@ -0,0 +1,207 @@
     2.4 +(*  Title:      HOL/Import/HOLLightInt.thy
     2.5 +    Author:     Cezary Kaliszyk
     2.6 +*)
     2.7 +
     2.8 +header {* Compatibility theorems for HOL Light integers *}
     2.9 +
    2.10 +theory HOLLightInt imports Main Real GCD begin
    2.11 +
    2.12 +fun int_coprime where "int_coprime ((a :: int), (b :: int)) = coprime a b"
    2.13 +
    2.14 +lemma DEF_int_coprime:
    2.15 +  "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
    2.16 +  apply (auto simp add: fun_eq_iff)
    2.17 +  apply (metis bezout_int zmult_commute)
    2.18 +  by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
    2.19 +
    2.20 +lemma INT_FORALL_POS:
    2.21 +  "(\<forall>n. P (int n)) = (\<forall>i\<ge>(int 0). P i)"
    2.22 +  by (auto, drule_tac x="nat i" in spec) simp
    2.23 +
    2.24 +lemma INT_LT_DISCRETE:
    2.25 +  "(x < y) = (x + int 1 \<le> y)"
    2.26 +  by auto
    2.27 +
    2.28 +lemma INT_ABS_MUL_1:
    2.29 +  "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
    2.30 +  by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult zmult_1_right)
    2.31 +
    2.32 +lemma dest_int_rep:
    2.33 +  "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
    2.34 +  by (metis (full_types) of_int_of_nat real_eq_of_int real_of_nat_def)
    2.35 +
    2.36 +lemma DEF_int_add:
    2.37 +  "op + = (\<lambda>u ua. floor (real u + real ua))"
    2.38 +  by simp
    2.39 +
    2.40 +lemma DEF_int_sub:
    2.41 +  "op - = (\<lambda>u ua. floor (real u - real ua))"
    2.42 +  by simp
    2.43 +
    2.44 +lemma DEF_int_mul:
    2.45 +  "op * = (\<lambda>u ua. floor (real u * real ua))"
    2.46 +  by (metis floor_number_of number_of_is_id number_of_real_def real_eq_of_int real_of_int_mult)
    2.47 +
    2.48 +lemma DEF_int_abs:
    2.49 +  "abs = (\<lambda>u. floor (abs (real u)))"
    2.50 +  by (metis floor_real_of_int real_of_int_abs)
    2.51 +
    2.52 +lemma DEF_int_sgn:
    2.53 +  "sgn = (\<lambda>u. floor (sgn (real u)))"
    2.54 +  by (simp add: sgn_if fun_eq_iff)
    2.55 +
    2.56 +lemma int_sgn_th:
    2.57 +  "real (sgn (x :: int)) = sgn (real x)"
    2.58 +  by (simp add: sgn_if)
    2.59 +
    2.60 +lemma DEF_int_max:
    2.61 +  "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
    2.62 +  by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max zle_linear)
    2.63 +
    2.64 +lemma int_max_th:
    2.65 +  "real (max (x :: int) y) = max (real x) (real y)"
    2.66 +  by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff zle_linear)
    2.67 +
    2.68 +lemma DEF_int_min:
    2.69 +  "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
    2.70 +  by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
    2.71 +
    2.72 +lemma int_min_th:
    2.73 +  "real (min (x :: int) y) = min (real x) (real y)"
    2.74 +  by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
    2.75 +
    2.76 +lemma INT_IMAGE:
    2.77 +  "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
    2.78 +  by (metis number_of_eq number_of_is_id of_int_of_nat)
    2.79 +
    2.80 +lemma DEF_int_pow:
    2.81 +  "op ^ = (\<lambda>u ua. floor (real u ^ ua))"
    2.82 +  by (simp add: floor_power)
    2.83 +
    2.84 +lemma DEF_int_divides:
    2.85 +  "op dvd = (\<lambda>(u :: int) ua. \<exists>x. ua = u * x)"
    2.86 +  by (metis dvdE dvdI)
    2.87 +
    2.88 +lemma DEF_int_divides':
    2.89 +  "(a :: int) dvd b = (\<exists>x. b = a * x)"
    2.90 +  by (metis dvdE dvdI)
    2.91 +
    2.92 +definition "int_mod (u :: int) ua ub = (u dvd (ua - ub))"
    2.93 +
    2.94 +lemma int_mod_def':
    2.95 +  "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
    2.96 +  by (simp add: int_mod_def_raw)
    2.97 +
    2.98 +lemma int_congruent:
    2.99 +  "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
   2.100 +  unfolding int_mod_def'
   2.101 +  by (auto simp add: DEF_int_divides')
   2.102 +
   2.103 +lemma int_congruent':
   2.104 +  "\<forall>(x :: int) y n. (n dvd x - y) = (\<exists>d. x - y = n * d)"
   2.105 +  using int_congruent[unfolded int_mod_def] .
   2.106 +
   2.107 +fun int_gcd where
   2.108 +  "int_gcd ((a :: int), (b :: int)) = gcd a b"
   2.109 +
   2.110 +definition "hl_mod (k\<Colon>int) (l\<Colon>int) = (if 0 \<le> l then k mod l else k mod - l)"
   2.111 +
   2.112 +lemma hl_mod_nonneg:
   2.113 +  "b \<noteq> 0 \<Longrightarrow> hl_mod a b \<ge> 0"
   2.114 +  by (simp add: hl_mod_def)
   2.115 +
   2.116 +lemma hl_mod_lt_abs:
   2.117 +  "b \<noteq> 0 \<Longrightarrow> hl_mod a b < abs b"
   2.118 +  by (simp add: hl_mod_def)
   2.119 +
   2.120 +definition "hl_div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
   2.121 +
   2.122 +lemma hl_mod_div:
   2.123 +  "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
   2.124 +  unfolding hl_div_def hl_mod_def
   2.125 +  by auto (metis zmod_zdiv_equality zmult_commute zmult_zminus)
   2.126 +
   2.127 +lemma sth:
   2.128 +  "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
   2.129 +   (\<forall>(x :: int) y. x + y = y + x) \<and>
   2.130 +   (\<forall>(x :: int). int 0 + x = x) \<and>
   2.131 +   (\<forall>(x :: int) y z. x * (y * z) = x * y * z) \<and>
   2.132 +   (\<forall>(x :: int) y. x * y = y * x) \<and>
   2.133 +   (\<forall>(x :: int). int 1 * x = x) \<and>
   2.134 +   (\<forall>(x :: int). int 0 * x = int 0) \<and>
   2.135 +   (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
   2.136 +   (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
   2.137 +  by (simp_all add: zadd_zmult_distrib2)
   2.138 +
   2.139 +lemma INT_DIVISION:
   2.140 +  "n ~= int 0 \<Longrightarrow> m = hl_div m n * n + hl_mod m n \<and> int 0 \<le> hl_mod m n \<and> hl_mod m n < abs n"
   2.141 +  by (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
   2.142 +
   2.143 +lemma INT_DIVMOD_EXIST_0:
   2.144 +  "\<exists>q r. if n = int 0 then q = int 0 \<and> r = m
   2.145 +         else int 0 \<le> r \<and> r < abs n \<and> m = q * n + r"
   2.146 +  apply (rule_tac x="hl_div m n" in exI)
   2.147 +  apply (rule_tac x="hl_mod m n" in exI)
   2.148 +  apply (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
   2.149 +  unfolding hl_div_def hl_mod_def
   2.150 +  by auto
   2.151 +
   2.152 +lemma DEF_div:
   2.153 +  "hl_div = (SOME q. \<exists>r. \<forall>m n. if n = int 0 then q m n = int 0 \<and> r m n = m
   2.154 +     else (int 0) \<le> (r m n) \<and> (r m n) < (abs n) \<and> m = ((q m n) * n) + (r m n))"
   2.155 +  apply (rule some_equality[symmetric])
   2.156 +  apply (rule_tac x="hl_mod" in exI)
   2.157 +  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
   2.158 +  apply (simp add: hl_div_def)
   2.159 +  apply (simp add: hl_mod_def)
   2.160 +  apply (drule_tac x="x" in spec)
   2.161 +  apply (drule_tac x="xa" in spec)
   2.162 +  apply (case_tac "0 = xa")
   2.163 +  apply (simp add: hl_mod_def hl_div_def)
   2.164 +  apply (case_tac "xa > 0")
   2.165 +  apply (simp add: hl_mod_def hl_div_def)
   2.166 +  apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le zadd_0 zdiv_eq_0_iff zmult_commute)
   2.167 +  apply (simp add: hl_mod_def hl_div_def)
   2.168 +  by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
   2.169 +
   2.170 +lemma DEF_rem:
   2.171 +  "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
   2.172 +     (if 0 \<le> n then m div n else - (m div - n)) = int 0 \<and> r m n = m
   2.173 +     else int 0 \<le> r m n \<and> r m n < abs n \<and>
   2.174 +            m = (if 0 \<le> n then m div n else - (m div - n)) * n + r m n)"
   2.175 +  apply (rule some_equality[symmetric])
   2.176 +  apply (fold hl_div_def)
   2.177 +  apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
   2.178 +  apply (simp add: hl_div_def)
   2.179 +  apply (simp add: hl_mod_def)
   2.180 +  apply (drule_tac x="x" in spec)
   2.181 +  apply (drule_tac x="xa" in spec)
   2.182 +  apply (case_tac "0 = xa")
   2.183 +  apply (simp add: hl_mod_def hl_div_def)
   2.184 +  apply (case_tac "xa > 0")
   2.185 +  apply (simp add: hl_mod_def hl_div_def)
   2.186 +  apply (metis add_left_cancel mod_div_equality)
   2.187 +  apply (simp add: hl_mod_def hl_div_def)
   2.188 +  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial zadd_commute zminus_zmod zmod_zminus2 zmult_commute)
   2.189 +
   2.190 +lemma DEF_int_gcd:
   2.191 +  "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
   2.192 +       (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
   2.193 +  apply (rule some_equality[symmetric])
   2.194 +  apply auto
   2.195 +  apply (metis bezout_int zmult_commute)
   2.196 +  apply (auto simp add: fun_eq_iff)
   2.197 +  apply (drule_tac x="a" in spec)
   2.198 +  apply (drule_tac x="b" in spec)
   2.199 +  using gcd_greatest_int zdvd_antisym_nonneg
   2.200 +  by auto
   2.201 +
   2.202 +definition "eqeq x y (r :: 'a \<Rightarrow> 'b \<Rightarrow> bool) = r x y"
   2.203 +
   2.204 +lemma INT_INTEGRAL:
   2.205 +  "(\<forall>x. int 0 * x = int 0) \<and>
   2.206 +   (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and>
   2.207 +   (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))"
   2.208 +  by (auto simp add: crossproduct_eq)
   2.209 +
   2.210 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Import/HOLLightList.thy	Wed Jul 13 00:23:24 2011 +0900
     3.3 @@ -0,0 +1,332 @@
     3.4 +(*  Title:      HOL/Import/HOLLightList.thy
     3.5 +    Author:     Cezary Kaliszyk
     3.6 +*)
     3.7 +
     3.8 +header {* Compatibility theorems for HOL Light lists *}
     3.9 +
    3.10 +theory HOLLightList
    3.11 +imports List
    3.12 +begin
    3.13 +
    3.14 +lemma AND_ALL2:
    3.15 +  "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m"
    3.16 +  by (induct l m rule: list_induct2') auto
    3.17 +
    3.18 +lemma MEM_EXISTS_EL:
    3.19 +  "(x \<in> set l) = (\<exists>i<length l. x = l ! i)"
    3.20 +  by (auto simp add: in_set_conv_nth)
    3.21 +
    3.22 +lemma INJECTIVE_MAP:
    3.23 +  "(\<forall>l m. map f l = map f m --> l = m) = (\<forall>x y. f x = f y --> x = y)"
    3.24 +proof (intro iffI allI impI)
    3.25 +  fix x y
    3.26 +  assume "\<forall>l m. map f l = map f m \<longrightarrow> l = m" "f x = f y"
    3.27 +  then show "x = y"
    3.28 +    by (drule_tac x="[x]" in spec) (drule_tac x="[y]" in spec, simp)
    3.29 +next
    3.30 +  fix l m
    3.31 +  assume a: "\<forall>x y. f x = f y \<longrightarrow> x = y"
    3.32 +  assume "map f l = map f m"
    3.33 +  then show "l = m"
    3.34 +    by (induct l m rule: list_induct2') (simp_all add: a)
    3.35 +qed
    3.36 +
    3.37 +lemma SURJECTIVE_MAP:
    3.38 +  "(\<forall>m. EX l. map f l = m) = (\<forall>y. EX x. f x = y)"
    3.39 +  apply (intro iffI allI)
    3.40 +  apply (drule_tac x="[y]" in spec)
    3.41 +  apply (elim exE)
    3.42 +  apply (case_tac l)
    3.43 +  apply simp
    3.44 +  apply (rule_tac x="a" in exI)
    3.45 +  apply simp
    3.46 +  apply (induct_tac m)
    3.47 +  apply simp
    3.48 +  apply (drule_tac x="a" in spec)
    3.49 +  apply (elim exE)
    3.50 +  apply (rule_tac x="x # l" in exI)
    3.51 +  apply simp
    3.52 +  done
    3.53 +
    3.54 +lemma LENGTH_TL:
    3.55 +  "l \<noteq> [] \<longrightarrow> length (tl l) = length l - 1"
    3.56 +  by simp
    3.57 +
    3.58 +lemma DEF_APPEND:
    3.59 +  "op @ = (SOME APPEND. (\<forall>l. APPEND [] l = l) \<and> (\<forall>h t l. APPEND (h # t) l = h # APPEND t l))"
    3.60 +  apply (rule some_equality[symmetric])
    3.61 +  apply (auto simp add: fun_eq_iff)
    3.62 +  apply (induct_tac x)
    3.63 +  apply simp_all
    3.64 +  done
    3.65 +
    3.66 +lemma DEF_REVERSE:
    3.67 +  "rev = (SOME REVERSE. REVERSE [] = [] \<and> (\<forall>l x. REVERSE (x # l) = (REVERSE l) @ [x]))"
    3.68 +  apply (rule some_equality[symmetric])
    3.69 +  apply (auto simp add: fun_eq_iff)
    3.70 +  apply (induct_tac x)
    3.71 +  apply simp_all
    3.72 +  done
    3.73 +
    3.74 +lemma DEF_LENGTH:
    3.75 +  "length = (SOME LENGTH. LENGTH [] = 0 \<and> (\<forall>h t. LENGTH (h # t) = Suc (LENGTH t)))"
    3.76 +  apply (rule some_equality[symmetric])
    3.77 +  apply (auto simp add: fun_eq_iff)
    3.78 +  apply (induct_tac x)
    3.79 +  apply simp_all
    3.80 +  done
    3.81 +
    3.82 +lemma DEF_MAP:
    3.83 +  "map = (SOME MAP. (\<forall>f. MAP f [] = []) \<and> (\<forall>f h t. MAP f (h # t) = f h # MAP f t))"
    3.84 +  apply (rule some_equality[symmetric])
    3.85 +  apply (auto simp add: fun_eq_iff)
    3.86 +  apply (induct_tac xa)
    3.87 +  apply simp_all
    3.88 +  done
    3.89 +
    3.90 +lemma DEF_REPLICATE:
    3.91 +  "replicate =
    3.92 +    (SOME REPLICATE. (\<forall>x. REPLICATE 0 x = []) \<and> (\<forall>n x. REPLICATE (Suc n) x = x # REPLICATE n x))"
    3.93 +  apply (rule some_equality[symmetric])
    3.94 +  apply (auto simp add: fun_eq_iff)
    3.95 +  apply (induct_tac x)
    3.96 +  apply simp_all
    3.97 +  done
    3.98 +
    3.99 +lemma DEF_ITLIST:
   3.100 +  "foldr = (SOME ITLIST. (\<forall>f b. ITLIST f [] b = b) \<and> (\<forall>h f t b. ITLIST f (h # t) b = f h (ITLIST f t b)))"
   3.101 +  apply (rule some_equality[symmetric])
   3.102 +  apply (auto simp add: fun_eq_iff)
   3.103 +  apply (induct_tac xa)
   3.104 +  apply simp_all
   3.105 +  done
   3.106 +
   3.107 +lemma DEF_ALL2: "list_all2 =
   3.108 +  (SOME ALL2.
   3.109 +    (\<forall>P l2. ALL2 P [] l2 = (l2 = [])) \<and>
   3.110 +    (\<forall>h1 P t1 l2.
   3.111 +      ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \<and> ALL2 P t1 (tl l2))))"
   3.112 +  apply (rule some_equality[symmetric])
   3.113 +  apply (auto)
   3.114 +  apply (case_tac l2, simp_all)
   3.115 +  apply (case_tac l2, simp_all)
   3.116 +  apply (case_tac l2, simp_all)
   3.117 +  apply (simp add: fun_eq_iff)
   3.118 +  apply (intro allI)
   3.119 +  apply (induct_tac xa xb rule: list_induct2')
   3.120 +  apply simp_all
   3.121 +  done
   3.122 +
   3.123 +lemma ALL2:
   3.124 + "list_all2 P [] [] = True \<and>
   3.125 +  list_all2 P (h1 # t1) [] = False \<and>
   3.126 +  list_all2 P [] (h2 # t2) = False \<and>
   3.127 +  list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \<and> list_all2 P t1 t2)"
   3.128 +  by simp
   3.129 +
   3.130 +lemma DEF_FILTER:
   3.131 +  "filter = (SOME FILTER. (\<forall>P. FILTER P [] = []) \<and>
   3.132 +     (\<forall>h P t. FILTER P (h # t) = (if P h then h # FILTER P t else FILTER P t)))"
   3.133 +  apply (rule some_equality[symmetric])
   3.134 +  apply (auto simp add: fun_eq_iff)
   3.135 +  apply (induct_tac xa)
   3.136 +  apply simp_all
   3.137 +  done
   3.138 +
   3.139 +fun map2 where
   3.140 +  "map2 f [] [] = []"
   3.141 +| "map2 f (h1 # t1) (h2 # t2) = (f h1 h2) # (map2 f t1 t2)"
   3.142 +
   3.143 +lemma MAP2:
   3.144 +  "map2 f [] [] = [] \<and> map2 f (h1 # t1) (h2 # t2) = f h1 h2 # map2 f t1 t2"
   3.145 +  by simp
   3.146 +
   3.147 +fun fold2 where
   3.148 +  "fold2 f [] [] b = b"
   3.149 +| "fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
   3.150 +
   3.151 +lemma ITLIST2:
   3.152 +  "fold2 f [] [] b = b \<and> fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
   3.153 +  by simp
   3.154 +
   3.155 +definition [simp]: "list_el x xs = nth xs x"
   3.156 +
   3.157 +lemma ZIP:
   3.158 +  "zip [] [] = [] \<and> zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)"
   3.159 +  by simp
   3.160 +
   3.161 +lemma LAST_CLAUSES:
   3.162 +  "last [h] = h \<and> last (h # k # t) = last (k # t)"
   3.163 +  by simp
   3.164 +
   3.165 +lemma DEF_NULL:
   3.166 +  "List.null = (SOME NULL. NULL [] = True \<and> (\<forall>h t. NULL (h # t) = False))"
   3.167 +  apply (rule some_equality[symmetric])
   3.168 +  apply (auto simp add: fun_eq_iff null_def)
   3.169 +  apply (case_tac x)
   3.170 +  apply simp_all
   3.171 +  done
   3.172 +
   3.173 +lemma DEF_ALL:
   3.174 +  "list_all = (SOME u. (\<forall>P. u P [] = True) \<and> (\<forall>h P t. u P (h # t) = (P h \<and> u P t)))"
   3.175 +  apply (rule some_equality[symmetric])
   3.176 +  apply auto[1]
   3.177 +  apply (simp add: fun_eq_iff)
   3.178 +  apply (intro allI)
   3.179 +  apply (induct_tac xa)
   3.180 +  apply simp_all
   3.181 +  done
   3.182 +
   3.183 +lemma MAP_EQ:
   3.184 +  "list_all (\<lambda>x. f x = g x) l \<longrightarrow> map f l = map g l"
   3.185 +  by (induct l) auto
   3.186 +
   3.187 +definition [simp]: "list_mem x xs = List.member xs x"
   3.188 +
   3.189 +lemma DEF_MEM:
   3.190 +  "list_mem = (SOME MEM. (\<forall>x. MEM x [] = False) \<and> (\<forall>h x t. MEM x (h # t) = (x = h \<or> MEM x t)))"
   3.191 +  apply (rule some_equality[symmetric])
   3.192 +  apply (auto simp add: member_def)[1]
   3.193 +  apply (simp add: fun_eq_iff)
   3.194 +  apply (intro allI)
   3.195 +  apply (induct_tac xa)
   3.196 +  apply (simp_all add: member_def)
   3.197 +  done
   3.198 +
   3.199 +lemma DEF_EX:
   3.200 +  "list_ex = (SOME u. (\<forall>P. u P [] = False) \<and> (\<forall>h P t. u P (h # t) = (P h \<or> u P t)))"
   3.201 +  apply (rule some_equality[symmetric])
   3.202 +  apply (auto)
   3.203 +  apply (simp add: fun_eq_iff)
   3.204 +  apply (intro allI)
   3.205 +  apply (induct_tac xa)
   3.206 +  apply (simp_all)
   3.207 +  done
   3.208 +
   3.209 +lemma ALL_IMP:
   3.210 +  "(\<forall>x. x \<in> set l \<and> P x \<longrightarrow> Q x) \<and> list_all P l \<longrightarrow> list_all Q l"
   3.211 +  by (simp add: list_all_iff)
   3.212 +
   3.213 +lemma NOT_EX: "(\<not> list_ex P l) = list_all (\<lambda>x. \<not> P x) l"
   3.214 +  by (simp add: list_all_iff list_ex_iff)
   3.215 +
   3.216 +lemma NOT_ALL: "(\<not> list_all P l) = list_ex (\<lambda>x. \<not> P x) l"
   3.217 +  by (simp add: list_all_iff list_ex_iff)
   3.218 +
   3.219 +lemma ALL_MAP: "list_all P (map f l) = list_all (P o f) l"
   3.220 +  by (simp add: list_all_iff)
   3.221 +
   3.222 +lemma ALL_T: "list_all (\<lambda>x. True) l"
   3.223 +  by (simp add: list_all_iff)
   3.224 +
   3.225 +lemma MAP_EQ_ALL2: "list_all2 (\<lambda>x y. f x = f y) l m \<longrightarrow> map f l = map f m"
   3.226 +  by (induct l m rule: list_induct2') simp_all
   3.227 +
   3.228 +lemma ALL2_MAP: "list_all2 P (map f l) l = list_all (\<lambda>a. P (f a) a) l"
   3.229 +  by (induct l) simp_all
   3.230 +
   3.231 +lemma MAP_EQ_DEGEN: "list_all (\<lambda>x. f x = x) l --> map f l = l"
   3.232 +  by (induct l) simp_all
   3.233 +
   3.234 +lemma ALL2_AND_RIGHT:
   3.235 +   "list_all2 (\<lambda>x y. P x \<and> Q x y) l m = (list_all P l \<and> list_all2 Q l m)"
   3.236 +  by (induct l m rule: list_induct2') auto
   3.237 +
   3.238 +lemma ITLIST_EXTRA:
   3.239 +  "foldr f (l @ [a]) b = foldr f l (f a b)"
   3.240 +  by simp
   3.241 +
   3.242 +lemma ALL_MP:
   3.243 +  "list_all (\<lambda>x. P x \<longrightarrow> Q x) l \<and> list_all P l \<longrightarrow> list_all Q l"
   3.244 +  by (simp add: list_all_iff)
   3.245 +
   3.246 +lemma AND_ALL:
   3.247 +  "(list_all P l \<and> list_all Q l) = list_all (\<lambda>x. P x \<and> Q x) l"
   3.248 +  by (auto simp add: list_all_iff)
   3.249 +
   3.250 +lemma EX_IMP:
   3.251 +  "(\<forall>x. x\<in>set l \<and> P x \<longrightarrow> Q x) \<and> list_ex P l \<longrightarrow> list_ex Q l"
   3.252 +  by (auto simp add: list_ex_iff)
   3.253 +
   3.254 +lemma ALL_MEM:
   3.255 +  "(\<forall>x. x\<in>set l \<longrightarrow> P x) = list_all P l"
   3.256 +  by (auto simp add: list_all_iff)
   3.257 +
   3.258 +lemma EX_MAP:
   3.259 +  "ALL P f l. list_ex P (map f l) = list_ex (P o f) l"
   3.260 +  by (simp add: list_ex_iff)
   3.261 +
   3.262 +lemma EXISTS_EX:
   3.263 +  "\<forall>P l. (EX x. list_ex (P x) l) = list_ex (\<lambda>s. EX x. P x s) l"
   3.264 +  by (auto simp add: list_ex_iff)
   3.265 +
   3.266 +lemma FORALL_ALL:
   3.267 +  "\<forall>P l. (\<forall>x. list_all (P x) l) = list_all (\<lambda>s. \<forall>x. P x s) l"
   3.268 +  by (auto simp add: list_all_iff)
   3.269 +
   3.270 +lemma MEM_APPEND: "\<forall>x l1 l2. (x\<in>set (l1 @ l2)) = (x\<in>set l1 \<or> x\<in>set l2)"
   3.271 +  by simp
   3.272 +
   3.273 +lemma MEM_MAP: "\<forall>f y l. (y\<in>set (map f l)) = (EX x. x\<in>set l \<and> y = f x)"
   3.274 +  by auto
   3.275 +
   3.276 +lemma MEM_FILTER: "\<forall>P l x. (x\<in>set (filter P l)) = (P x \<and> x\<in>set l)"
   3.277 +  by auto
   3.278 +
   3.279 +lemma EX_MEM: "(EX x. P x \<and> x\<in>set l) = list_ex P l"
   3.280 +  by (auto simp add: list_ex_iff)
   3.281 +
   3.282 +lemma ALL2_MAP2:
   3.283 +  "list_all2 P (map f l) (map g m) = list_all2 (\<lambda>x y. P (f x) (g y)) l m"
   3.284 +  by (simp add: list_all2_map1 list_all2_map2)
   3.285 +
   3.286 +lemma ALL2_ALL:
   3.287 +  "list_all2 P l l = list_all (\<lambda>x. P x x) l"
   3.288 +  by (induct l) simp_all
   3.289 +
   3.290 +lemma LENGTH_MAP2:
   3.291 +  "length l = length m \<longrightarrow> length (map2 f l m) = length m"
   3.292 +  by (induct l m rule: list_induct2') simp_all
   3.293 +
   3.294 +lemma DEF_set_of_list:
   3.295 +  "set = (SOME sol. sol [] = {} \<and> (\<forall>h t. sol (h # t) = insert h (sol t)))"
   3.296 +  apply (rule some_equality[symmetric])
   3.297 +  apply (simp_all)
   3.298 +  apply (rule ext)
   3.299 +  apply (induct_tac x)
   3.300 +  apply simp_all
   3.301 +  done
   3.302 +
   3.303 +lemma IN_SET_OF_LIST:
   3.304 +  "ALL x l. (x\<in>set l) = list_mem x l"
   3.305 +  by (simp add: member_def)
   3.306 +
   3.307 +lemma DEF_BUTLAST:
   3.308 +  "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"
   3.309 +  apply (rule some_equality[symmetric])
   3.310 +  apply auto
   3.311 +  apply (rule ext)
   3.312 +  apply (induct_tac x)
   3.313 +  apply auto
   3.314 +  done
   3.315 +
   3.316 +lemma MONO_ALL:
   3.317 +  "(ALL x. P x \<longrightarrow> Q x) \<longrightarrow> list_all P l \<longrightarrow> list_all Q l"
   3.318 +  by (simp add: list_all_iff)
   3.319 +
   3.320 +lemma EL_TL: "l \<noteq> [] \<Longrightarrow> tl l ! x = l ! (x + 1)"
   3.321 +  by (induct l) (simp_all)
   3.322 +
   3.323 +(* Assume the same behaviour outside of the usual domain.
   3.324 +   For HD, LAST, EL it follows from "undefined = SOME _. False".
   3.325 +
   3.326 +   The definitions of TL and ZIP are different for empty lists.
   3.327 + *)
   3.328 +axioms
   3.329 +  DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
   3.330 +  DEF_LAST: "last =
   3.331 +    (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
   3.332 +  DEF_EL: "list_el =
   3.333 +    (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
   3.334 +
   3.335 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Import/HOLLightReal.thy	Wed Jul 13 00:23:24 2011 +0900
     4.3 @@ -0,0 +1,331 @@
     4.4 +(*  Title:      HOL/Import/HOLLightReal.thy
     4.5 +    Author:     Cezary Kaliszyk
     4.6 +*)
     4.7 +
     4.8 +header {* Compatibility theorems for HOL Light reals *}
     4.9 +
    4.10 +theory HOLLightReal imports Real begin
    4.11 +
    4.12 +lemma REAL_OF_NUM_MAX:
    4.13 +  "max (real (m :: nat)) (real n) = real (max m n)"
    4.14 +  by simp
    4.15 +
    4.16 +lemma REAL_OF_NUM_MIN:
    4.17 +  "min (real (m :: nat)) (real n) = real (min m n)"
    4.18 +  by simp
    4.19 +
    4.20 +lemma REAL_POLY_NEG_CLAUSES:
    4.21 +  "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
    4.22 +  by simp
    4.23 +
    4.24 +lemma REAL_MUL_AC:
    4.25 +  "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
    4.26 +  by simp
    4.27 +
    4.28 +lemma REAL_EQ_ADD_LCANCEL_0:
    4.29 +  "((x :: real) + y = x) = (y = 0)"
    4.30 +  by simp
    4.31 +
    4.32 +lemma REAL_EQ_ADD_RCANCEL_0:
    4.33 +  "((x :: real) + y = y) = (x = 0)"
    4.34 +  by simp
    4.35 +
    4.36 +lemma REAL_LT_ANTISYM:
    4.37 +  "\<not> ((x :: real) < y \<and> y < x)"
    4.38 +  by simp
    4.39 +
    4.40 +lemma REAL_LET_ANTISYM:
    4.41 +  "\<not> ((x :: real) \<le> y \<and> y < x)"
    4.42 +  by simp
    4.43 +
    4.44 +lemma REAL_LT_NEGTOTAL:
    4.45 +  "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
    4.46 +  by auto
    4.47 +
    4.48 +lemma REAL_LT_ADDNEG:
    4.49 +  "((y :: real) < x + - z) = (y + z < x)"
    4.50 +  by auto
    4.51 +
    4.52 +lemma REAL_LT_ADDNEG2:
    4.53 +  "((x :: real) + - y < z) = (x < z + y)"
    4.54 +  by auto
    4.55 +
    4.56 +lemma REAL_LT_ADD1:
    4.57 +  "(x :: real) \<le> y \<longrightarrow> x < y + 1"
    4.58 +  by simp
    4.59 +
    4.60 +lemma REAL_SUB_ADD2:
    4.61 +  "(y :: real) + (x - y) = x"
    4.62 +  by simp
    4.63 +
    4.64 +lemma REAL_ADD_SUB:
    4.65 +  "(x :: real) + y - x = y"
    4.66 +  by simp
    4.67 +
    4.68 +lemma REAL_NEG_EQ:
    4.69 +  "(- (x :: real) = y) = (x = - y)"
    4.70 +  by auto
    4.71 +
    4.72 +lemma REAL_LE_ADDR:
    4.73 +  "((x :: real) \<le> x + y) = (0 \<le> y)"
    4.74 +  by simp
    4.75 +
    4.76 +lemma REAL_LE_ADDL:
    4.77 +  "((y :: real) \<le> x + y) = (0 \<le> x)"
    4.78 +  by simp
    4.79 +
    4.80 +lemma REAL_LT_ADDR:
    4.81 +  "((x :: real) < x + y) = (0 < y)"
    4.82 +  by simp
    4.83 +
    4.84 +lemma REAL_LT_ADDL:
    4.85 +  "((y :: real) < x + y) = (0 < x)"
    4.86 +  by simp
    4.87 +
    4.88 +lemma REAL_SUB_SUB:
    4.89 +  "(x :: real) - y - x = - y"
    4.90 +  by simp
    4.91 +
    4.92 +lemma REAL_SUB_LNEG:
    4.93 +  "- (x :: real) - y = - (x + y)"
    4.94 +  by simp
    4.95 +
    4.96 +lemma REAL_SUB_NEG2:
    4.97 +  "- (x :: real) - - y = y - x"
    4.98 +  by simp
    4.99 +
   4.100 +lemma REAL_SUB_TRIANGLE:
   4.101 +  "(a :: real) - b + (b - c) = a - c"
   4.102 +  by simp
   4.103 +
   4.104 +lemma REAL_SUB_SUB2:
   4.105 +  "(x :: real) - (x - y) = y"
   4.106 +  by simp
   4.107 +
   4.108 +lemma REAL_ADD_SUB2:
   4.109 +  "(x :: real) - (x + y) = - y"
   4.110 +  by simp
   4.111 +
   4.112 +lemma REAL_POS_NZ:
   4.113 +  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
   4.114 +  by simp
   4.115 +
   4.116 +lemma REAL_DIFFSQ:
   4.117 +  "((x :: real) + y) * (x - y) = x * x - y * y"
   4.118 +  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
   4.119 +
   4.120 +lemma REAL_ABS_TRIANGLE_LE:
   4.121 +  "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
   4.122 +  by auto
   4.123 +
   4.124 +lemma REAL_ABS_TRIANGLE_LT:
   4.125 +  "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
   4.126 +  by auto
   4.127 +
   4.128 +lemma REAL_ABS_REFL:
   4.129 +  "(abs (x :: real) = x) = (0 \<le> x)"
   4.130 +  by auto
   4.131 +
   4.132 +lemma REAL_ABS_BETWEEN:
   4.133 +  "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
   4.134 +  by auto
   4.135 +
   4.136 +lemma REAL_ABS_BOUND:
   4.137 +  "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
   4.138 +  by auto
   4.139 +
   4.140 +lemma REAL_ABS_STILLNZ:
   4.141 +  "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
   4.142 +  by auto
   4.143 +
   4.144 +lemma REAL_ABS_CASES:
   4.145 +  "(x :: real) = 0 \<or> 0 < abs x"
   4.146 +  by simp
   4.147 +
   4.148 +lemma REAL_ABS_BETWEEN1:
   4.149 +  "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
   4.150 +  by auto
   4.151 +
   4.152 +lemma REAL_ABS_SIGN:
   4.153 +  "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
   4.154 +  by auto
   4.155 +
   4.156 +lemma REAL_ABS_SIGN2:
   4.157 +  "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
   4.158 +  by auto
   4.159 +
   4.160 +lemma REAL_ABS_CIRCLE:
   4.161 +  "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
   4.162 +  by auto
   4.163 +
   4.164 +lemma REAL_BOUNDS_LT:
   4.165 +  "(- (k :: real) < x \<and> x < k) = (abs x < k)"
   4.166 +  by auto
   4.167 +
   4.168 +lemma REAL_MIN_MAX:
   4.169 +  "min (x :: real) y = - max (- x) (- y)"
   4.170 +  by auto
   4.171 +
   4.172 +lemma REAL_MAX_MIN:
   4.173 +  "max (x :: real) y = - min (- x) (- y)"
   4.174 +  by auto
   4.175 +
   4.176 +lemma REAL_MAX_MAX:
   4.177 +  "(x :: real) \<le> max x y \<and> y \<le> max x y"
   4.178 +  by simp
   4.179 +
   4.180 +lemma REAL_MIN_MIN:
   4.181 +  "min (x :: real) y \<le> x \<and> min x y \<le> y"
   4.182 +  by simp
   4.183 +
   4.184 +lemma REAL_MAX_ACI:
   4.185 +  "max (x :: real) y = max y x \<and>
   4.186 +   max (max x y) z = max x (max y z) \<and>
   4.187 +   max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
   4.188 +  by auto
   4.189 +
   4.190 +
   4.191 +lemma REAL_MIN_ACI:
   4.192 +  "min (x :: real) y = min y x \<and>
   4.193 +   min (min x y) z = min x (min y z) \<and>
   4.194 +   min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
   4.195 +  by auto
   4.196 +
   4.197 +lemma REAL_EQ_MUL_RCANCEL:
   4.198 +  "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
   4.199 +  by auto
   4.200 +
   4.201 +lemma REAL_MUL_LINV_UNIQ:
   4.202 +  "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
   4.203 +  by (metis inverse_inverse_eq inverse_unique)
   4.204 +
   4.205 +lemma REAL_DIV_RMUL:
   4.206 +  "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
   4.207 +  by simp
   4.208 +
   4.209 +lemma REAL_DIV_LMUL:
   4.210 +  "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
   4.211 +  by simp
   4.212 +
   4.213 +lemma REAL_LT_IMP_NZ:
   4.214 +  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
   4.215 +  by simp
   4.216 +
   4.217 +lemma REAL_LT_LCANCEL_IMP:
   4.218 +  "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
   4.219 +  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
   4.220 +
   4.221 +lemma REAL_LT_RCANCEL_IMP:
   4.222 +  "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
   4.223 +  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
   4.224 +
   4.225 +lemma REAL_MUL_POS_LE:
   4.226 +  "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
   4.227 +  by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
   4.228 +
   4.229 +lemma REAL_EQ_RDIV_EQ:
   4.230 +  "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
   4.231 +  by auto
   4.232 +
   4.233 +lemma REAL_EQ_LDIV_EQ:
   4.234 +  "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
   4.235 +  by auto
   4.236 +
   4.237 +lemma REAL_SUB_INV:
   4.238 +  "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
   4.239 +  by (simp add: division_ring_inverse_diff real_divide_def)
   4.240 +
   4.241 +lemma REAL_DOWN:
   4.242 +  "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
   4.243 +  by (intro impI exI[of _ "d / 2"]) simp
   4.244 +
   4.245 +lemma REAL_POW_MONO_LT:
   4.246 +  "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
   4.247 +  by simp
   4.248 +
   4.249 +lemma REAL_POW_MONO:
   4.250 +  "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
   4.251 +  by (cases "m < n", cases "x = 1") auto
   4.252 +
   4.253 +lemma REAL_EQ_LCANCEL_IMP:
   4.254 +  "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
   4.255 +  by auto
   4.256 +
   4.257 +lemma REAL_LE_DIV:
   4.258 +  "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
   4.259 +  by (simp add: zero_le_divide_iff)
   4.260 +
   4.261 +lemma REAL_10: "(1::real) \<noteq> 0"
   4.262 +  by simp
   4.263 +
   4.264 +lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
   4.265 +  by simp
   4.266 +
   4.267 +lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
   4.268 +  by simp
   4.269 +
   4.270 +lemma REAL_ADD_LINV:  "-x + x = (0::real)"
   4.271 +  by simp
   4.272 +
   4.273 +lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
   4.274 +  by simp
   4.275 +
   4.276 +lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
   4.277 +  by auto
   4.278 +
   4.279 +lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
   4.280 +  by auto
   4.281 +
   4.282 +lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
   4.283 +  by (simp add: real_of_nat_Suc)
   4.284 +
   4.285 +lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
   4.286 +  by (simp add: abs_if)
   4.287 +
   4.288 +lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
   4.289 +  by simp
   4.290 +
   4.291 +lemma REAL_POLY_CLAUSES:
   4.292 +  "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
   4.293 +   (\<forall>(x :: real) y. x + y = y + x) \<and>
   4.294 +   (\<forall>(x :: real). 0 + x = x) \<and>
   4.295 +   (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
   4.296 +   (\<forall>(x :: real) y. x * y = y * x) \<and>
   4.297 +   (\<forall>(x :: real). 1 * x = x) \<and>
   4.298 +   (\<forall>(x :: real). 0 * x = 0) \<and>
   4.299 +   (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
   4.300 +   (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
   4.301 +  by (auto simp add: mult.add_right)
   4.302 +
   4.303 +lemma REAL_COMPLETE:
   4.304 +  "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
   4.305 +   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
   4.306 +          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
   4.307 +  apply (intro allI impI, elim conjE)
   4.308 +  apply (drule complete_real[unfolded Ball_def mem_def])
   4.309 +  apply simp_all
   4.310 +  done
   4.311 +
   4.312 +lemma REAL_COMPLETE_SOMEPOS:
   4.313 +  "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
   4.314 +   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
   4.315 +          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
   4.316 +  using REAL_COMPLETE by auto
   4.317 +
   4.318 +lemma REAL_ADD_AC:
   4.319 +  "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
   4.320 +  by simp
   4.321 +
   4.322 +lemma REAL_LE_RNEG:
   4.323 +  "((x :: real) \<le> - y) = (x + y \<le> 0)"
   4.324 +  by auto
   4.325 +
   4.326 +lemma REAL_LE_NEGTOTAL:
   4.327 +  "0 \<le> (x :: real) \<or> 0 \<le> - x"
   4.328 +  by auto
   4.329 +
   4.330 +lemma DEF_real_sgn:
   4.331 +  "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
   4.332 +  by (simp add: ext)
   4.333 +
   4.334 +end
     5.1 --- a/src/HOL/Import/hol4rews.ML	Tue Jul 12 16:00:05 2011 +0900
     5.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Jul 13 00:23:24 2011 +0900
     5.3 @@ -160,13 +160,16 @@
     5.4      let
     5.5          val _ = message "Adding HOL4 rewrite"
     5.6          val th1 = th RS @{thm eq_reflection}
     5.7 +                  handle _ => th
     5.8          val current_rews = HOL4Rewrites.get thy
     5.9          val new_rews = insert Thm.eq_thm th1 current_rews
    5.10          val updated_thy  = HOL4Rewrites.put new_rews thy
    5.11      in
    5.12          (Context.Theory updated_thy,th1)
    5.13      end
    5.14 -  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
    5.15 +  | add_hol4_rewrite (context, th) = (context,
    5.16 +      (th RS @{thm eq_reflection} handle _ => th)
    5.17 +    );
    5.18  
    5.19  fun ignore_hol4 bthy bthm thy =
    5.20      let
     6.1 --- a/src/HOL/Import/import_syntax.ML	Tue Jul 12 16:00:05 2011 +0900
     6.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jul 13 00:23:24 2011 +0900
     6.3 @@ -58,7 +58,7 @@
     6.4                      let
     6.5                          val _ = ImportRecorder.load_history thyname
     6.6                          val thy = Replay.import_thms thyname int_thms thmnames thy
     6.7 -                            handle x => (ImportRecorder.save_history thyname; raise x)  (* FIXME avoid handle x ?? *)
     6.8 +                            (*handle x => (ImportRecorder.save_history thyname; raise x)*)  (* FIXME avoid handle x ?? *)
     6.9                          val _ = ImportRecorder.save_history thyname
    6.10                          val _ = ImportRecorder.clear_history ()
    6.11                      in
     7.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jul 12 16:00:05 2011 +0900
     7.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jul 13 00:23:24 2011 +0900
     7.3 @@ -187,60 +187,63 @@
     7.4  fun quotename c =
     7.5    if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
     7.6  
     7.7 -fun simple_smart_string_of_cterm ctxt0 ct =
     7.8 -    let
     7.9 -        val ctxt = ctxt0
    7.10 -          |> Config.put show_brackets false
    7.11 -          |> Config.put show_all_types true
    7.12 -          |> Config.put show_sorts true
    7.13 -          |> Config.put Syntax.ambiguity_enabled true;
    7.14 -        val {t,T,...} = rep_cterm ct
    7.15 -        (* Hack to avoid parse errors with Trueprop *)
    7.16 -        val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    7.17 -                           handle TERM _ => ct
    7.18 -    in
    7.19 -        quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
    7.20 -    end
    7.21 +exception SMART_STRING
    7.22  
    7.23 -exception SMART_STRING
    7.24 +fun no_vars context tm =
    7.25 +  let
    7.26 +    val ctxt = Variable.set_body false context;
    7.27 +    val ([tm'], _) = Variable.import_terms true [tm] ctxt;
    7.28 +  in tm' end
    7.29  
    7.30  fun smart_string_of_cterm ctxt0 ct =
    7.31      let
    7.32 -        val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
    7.33 +        val ctxt = ctxt0
    7.34 +          |> Config.put Syntax.ambiguity_enabled true
    7.35 +          |> Config.put show_brackets false
    7.36 +          |> Config.put show_all_types false
    7.37 +          |> Config.put show_types false
    7.38 +          |> Config.put show_sorts false;
    7.39          val {t,T,...} = rep_cterm ct
    7.40          (* Hack to avoid parse errors with Trueprop *)
    7.41 -        val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    7.42 -                   handle TERM _ => ct
    7.43 -        fun match u = t aconv u
    7.44 -        fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
    7.45 -          | G 1 f ctxt x = G 0 f (Config.put show_brackets true ctxt) x
    7.46 -          | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
    7.47 -          | G 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
    7.48 +        val t' = HOLogic.dest_Trueprop t
    7.49 +                 handle TERM _ => t
    7.50 +        val tn = no_vars ctxt t'
    7.51 +        fun match u =
    7.52 +            let val _ = Thm.match (ct, cterm_of (Proof_Context.theory_of ctxt) u) in true end
    7.53 +            handle MATCH => false
    7.54 +        fun G 0 f ctxt x = f ctxt x
    7.55 +          | G 1 f ctxt x = f (Config.put show_types true ctxt) x
    7.56 +          | G 2 f ctxt x = G 1 f (Config.put show_sorts true ctxt) x
    7.57 +          | G 3 f ctxt x = G 2 f (Config.put show_all_types true ctxt) x
    7.58 +          | G 4 f ctxt x = G 3 f (Config.put show_brackets true ctxt) x
    7.59            | G _ _ _ _ = raise SMART_STRING
    7.60          fun F n =
    7.61              let
    7.62 -                val str =
    7.63 -                  G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
    7.64 +                val str = G n Syntax.string_of_term ctxt tn
    7.65 +                val _ = warning (PolyML.makestring (n, str))
    7.66                  val u = Syntax.parse_term ctxt str
    7.67 -                  |> Type.constraint T |> Syntax.check_term ctxt
    7.68 +                val u = if t = t' then u else HOLogic.mk_Trueprop u
    7.69 +                val u = Syntax.check_term ctxt (Type.constraint T u)
    7.70              in
    7.71                  if match u
    7.72                  then quote str
    7.73                  else F (n+1)
    7.74              end
    7.75 -            handle ERROR mesg => F (n + 1)
    7.76 +            handle ERROR _ => F (n + 1)
    7.77                | SMART_STRING =>
    7.78 -                  error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
    7.79 +                  let val _ =
    7.80 +                    warning ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
    7.81 +                  in quote (G 2 Syntax.string_of_term ctxt tn) end
    7.82      in
    7.83        Print_Mode.setmp [] F 0
    7.84      end
    7.85 -    handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
    7.86  
    7.87  fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
    7.88  
    7.89  fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
    7.90 +val topctxt = ML_Context.the_local_context ();
    7.91  fun prin t = writeln (Print_Mode.setmp []
    7.92 -  (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
    7.93 +  (fn () => Syntax.string_of_term topctxt t) ());
    7.94  fun pth (HOLThm(ren,thm)) =
    7.95      let
    7.96          (*val _ = writeln "Renaming:"
    7.97 @@ -1363,6 +1366,7 @@
    7.98          val thy' = add_hol4_pending thyname thmname args thy
    7.99          val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   7.100          val th = disambiguate_frees th
   7.101 +        val th = Object_Logic.rulify th
   7.102          val thy2 =
   7.103            if gen_output
   7.104            then