HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Tue Jul 12 16:00:05 2011 +0900
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Wed Jul 13 00:23:24 2011 +0900
@@ -1,104 +1,212 @@
(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy
Author: Steven Obua, TU Muenchen
+ Author: Cezary Kaliszyk
*)
-theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
+theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
-(*;skip_import_dir "/home/obua/tmp/cache"
-
-;skip_import on*)
+;import_segment "hollight"
-;import_segment "hollight";
-
-setup_dump "../HOLLight" "HOLLight";
+;setup_dump "../HOLLight" "HOLLight";
-append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
+;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *}
-;import_theory hollight;
+;import_theory hollight
-ignore_thms
- TYDEF_1
- DEF_one
- TYDEF_prod
- TYDEF_num
- IND_SUC_0_EXISTS
- DEF__0
- DEF_SUC
- DEF_IND_SUC
- DEF_IND_0
- DEF_NUM_REP
- TYDEF_sum
- DEF_INL
- DEF_INR
- (* TYDEF_option*);
+;ignore_thms
+ (* Unit type *)
+ TYDEF_1 DEF_one
+ (* Product type *)
+ TYDEF_prod "DEF_," DEF_mk_pair REP_ABS_PAIR
+ (* Option type *)
+ TYDEF_option DEF_NONE DEF_SOME
+ (* Sum type *)
+ TYDEF_sum DEF_INL DEF_INR DEF_OUTL DEF_OUTR
+ (* Naturals *)
+ TYDEF_num DEF__0 DEF_SUC
+ (* Lists *)
+ TYDEF_list DEF_NIL DEF_CONS DEF_HD DEF_TL DEF_MAP2 DEF_ITLIST2 ALL_MAP EX_MAP
+ DEF_ASSOC MEM_ASSOC DEF_ZIP EL_TL
-type_maps
- ind > Nat.ind
- bool > bool
- fun > fun
+ (* list_of_set uses Isabelle lists with HOLLight CARD *)
+ DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
+ MEM_LIST_OF_SET FINITE_SET_OF_LIST
+ (* UNIV *)
+ DIMINDEX_FINITE_SUM DIMINDEX_HAS_SIZE_FINITE_SUM
+ FSTCART_PASTECART SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
+ (* Reals *)
+ (* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
+ DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
+ (* Integers *)
+ (* TYDEF_int DEF_int_divides DEF_int_coprime*)
+
+;type_maps
+ bool > HOL.bool
+ "fun" > "fun"
N_1 > Product_Type.unit
prod > Product_Type.prod
+ ind > Nat.ind
num > Nat.nat
sum > Sum_Type.sum
-(* option > Datatype.option*);
+ option > Datatype.option
+ list > List.list
+(*real > RealDef.real *)
+(*int > Int.int *)
-const_renames
+;const_renames
"==" > "eqeq"
- ".." > "dotdot"
- "ALL" > ALL_list;
+ "ALL" > list_ALL
+ "EX" > list_EX
-const_maps
- T > True
- F > False
- ONE_ONE > HOL4Setup.ONE_ONE
- ONTO > Fun.surj
+;const_maps
+ T > HOL.True
+ F > HOL.False
"=" > HOL.eq
"==>" > HOL.implies
"/\\" > HOL.conj
"\\/" > HOL.disj
- "!" > All
- "?" > Ex
- "?!" > Ex1
- "~" > Not
+ "!" > HOL.All
+ "?" > HOL.Ex
+ "?!" > HOL.Ex1
+ "~" > HOL.Not
+ COND > HOL.If
+ ONE_ONE > Fun.inj
+ ONTO > Fun.surj
o > Fun.comp
- "@" > "Hilbert_Choice.Eps"
+ "@" > Hilbert_Choice.Eps
+ CHOICE > Hilbert_Choice.Eps
I > Fun.id
one > Product_Type.Unity
- LET > HOL4Compat.LET
+ LET > HOLLightCompat.LET
mk_pair > Product_Type.Pair_Rep
- "," > Pair
- REP_prod > Rep_Prod
- ABS_prod > Abs_Prod
- FST > fst
- SND > snd
- "_0" > 0 :: nat
- SUC > Suc
+ "," > Product_Type.Pair
+ FST > Product_Type.fst
+ SND > Product_Type.snd
+ CURRY > Product_Type.curry
+ "_0" > Groups.zero_class.zero :: nat
+ SUC > Nat.Suc
PRE > HOLLightCompat.Pred
- NUMERAL > HOL4Compat.NUMERAL
- "+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- "-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ NUMERAL > HOLLightCompat.NUMERAL
+ mk_num > Fun.id
+ "+" > 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"
+ "<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ "<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ ">" > Orderings.ord_class.greater :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ ">=" > Orderings.ord_class.greater_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ MIN > Orderings.ord_class.min :: "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"
BIT0 > HOLLightCompat.NUMERAL_BIT0
- BIT1 > HOL4Compat.NUMERAL_BIT1
+ BIT1 > HOLLightCompat.NUMERAL_BIT1
INL > Sum_Type.Inl
INR > Sum_Type.Inr
- (* NONE > Datatype.None
- SOME > Datatype.Some;
- HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
-
-(*import_until "TYDEF_sum"
-
-consts
-print_theorems
+ OUTL > HOLLightCompat.OUTL
+ OUTR > HOLLightCompat.OUTR
+ NONE > Datatype.None
+ SOME > Datatype.Some
+ EVEN > Parity.even_odd_class.even :: "nat \<Rightarrow> bool"
+ ODD > HOLLightCompat.ODD
+ FACT > Fact.fact_class.fact :: "nat \<Rightarrow> nat"
+ WF > Wellfounded.wfP
+ NIL > List.list.Nil
+ CONS > List.list.Cons
+ APPEND > List.append
+ REVERSE > List.rev
+ LENGTH > List.length
+ MAP > List.map
+ LAST > List.last
+ BUTLAST > List.butlast
+ REPLICATE > List.replicate
+ ITLIST > List.foldr
+ list_ALL > List.list_all
+ ALL2 > List.list_all2
+ list_EX > List.list_ex
+ FILTER > List.filter
+ NULL > List.null
+ HD > List.hd
+ TL > List.tl
+ EL > HOLLightList.list_el
+ ZIP > List.zip
+ MAP2 > HOLLightList.map2
+ ITLIST2 > HOLLightList.fold2
+ MEM > HOLLightList.list_mem
+ set_of_list > List.set
+ IN > Set.member
+ INSERT > Set.insert
+ EMPTY > Orderings.bot_class.bot :: "'a \<Rightarrow> bool"
+ GABS > Hilbert_Choice.Eps
+ GEQ > HOL.eq
+ GSPEC > Set.Collect
+ SETSPEC > HOLLightCompat.SETSPEC
+ UNION > Lattices.semilattice_sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ INTER > Lattices.semilattice_inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+ PSUBSET > Orderings.ord_class.less :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+ DELETE > HOLLightCompat.DELETE
+ DISJOINT > HOLLightCompat.DISJOINT
+ IMAGE > Set.image
+ FINITE > Finite_Set.finite
+ INFINITE > HOLLightCompat.INFINITE
+ ".." > HOLLightCompat.dotdot
+ UNIV > Orderings.top_class.top :: "'a \<Rightarrow> bool"
+ MEASURE > HOLLightCompat.MEASURE
+(*real_of_num > RealDef.real :: "nat => real"
+ real_neg > Groups.uminus_class.uminus :: "real => real"
+ real_inv > Rings.inverse_class.inverse :: "real => real"
+ real_add > Groups.plus_class.plus :: "real => real => real"
+ real_sub > Groups.minus_class.minus :: "real => real => real"
+ real_mul > Groups.times_class.times :: "real => real => real"
+ real_div > Rings.inverse_class.divide :: "real => real => real"
+ real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
+ real_le > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
+ real_gt > Orderings.ord_class.greater :: "real \<Rightarrow> real \<Rightarrow> bool"
+ real_ge > Orderings.ord_class.greater_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
+ real_pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
+ real_abs > Groups.abs_class.abs :: "real \<Rightarrow> real"
+ real_max > Orderings.ord_class.max :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_min > Orderings.ord_class.min :: "real \<Rightarrow> real \<Rightarrow> real"
+ real_sgn > Groups.sgn_class.sgn :: "real \<Rightarrow> real"*)
+(*real_of_int > RealDef.real :: "int => real"
+ int_of_real > Archimedean_Field.floor :: "real \<Rightarrow> int"
+ dest_int > RealDef.real :: "int => real"
+ mk_int > Archimedean_Field.floor :: "real \<Rightarrow> int"
+ int_lt > Orderings.ord_class.less :: "int \<Rightarrow> int \<Rightarrow> bool"
+ int_le > Orderings.ord_class.less_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
+ int_gt > Orderings.ord_class.greater :: "int \<Rightarrow> int \<Rightarrow> bool"
+ int_ge > Orderings.ord_class.greater_eq :: "int \<Rightarrow> int \<Rightarrow> bool"
+ int_of_num > Nat.semiring_1_class.of_nat :: "nat \<Rightarrow> int"
+ int_neg > Groups.uminus_class.uminus :: "int \<Rightarrow> int"
+ int_add > Groups.plus_class.plus :: "int => int => int"
+ int_sub > Groups.minus_class.minus :: "int => int => int"
+ int_mul > Groups.times_class.times :: "int => int => int"
+ int_abs > Groups.abs_class.abs :: "int \<Rightarrow> int"
+ int_max > Orderings.ord_class.max :: "int \<Rightarrow> int \<Rightarrow> int"
+ int_min > Orderings.ord_class.min :: "int \<Rightarrow> int \<Rightarrow> int"
+ int_sgn > Groups.sgn_class.sgn :: "int \<Rightarrow> int"
+ int_pow > Power.power_class.power :: "int \<Rightarrow> nat \<Rightarrow> int"
+ int_div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
+ div > HOLLightInt.hl_div :: "int \<Rightarrow> int \<Rightarrow> int"
+ mod_int > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+ rem > HOLLightInt.hl_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+ int_divides > Rings.dvd_class.dvd :: "int \<Rightarrow> int \<Rightarrow> bool"
+ int_mod > HOLLightInt.int_mod :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
+ int_gcd > HOLLightInt.int_gcd :: "int \<times> int \<Rightarrow> int"
+ int_coprime > HOLLightInt.int_coprime :: "int \<times> int \<Rightarrow> bool"
+ eqeq > HOLLightInt.eqeq*)
-import_until *)
+;end_import
-end_import;
+;append_dump "end"
-append_dump "end";
+;flush_dump
-flush_dump;
-
-import_segment "";
+;import_segment ""
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOLLightInt.thy Wed Jul 13 00:23:24 2011 +0900
@@ -0,0 +1,207 @@
+(* Title: HOL/Import/HOLLightInt.thy
+ Author: Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light integers *}
+
+theory HOLLightInt imports Main Real GCD begin
+
+fun int_coprime where "int_coprime ((a :: int), (b :: int)) = coprime a b"
+
+lemma DEF_int_coprime:
+ "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
+ apply (auto simp add: fun_eq_iff)
+ apply (metis bezout_int zmult_commute)
+ by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
+
+lemma INT_FORALL_POS:
+ "(\<forall>n. P (int n)) = (\<forall>i\<ge>(int 0). P i)"
+ by (auto, drule_tac x="nat i" in spec) simp
+
+lemma INT_LT_DISCRETE:
+ "(x < y) = (x + int 1 \<le> y)"
+ by auto
+
+lemma INT_ABS_MUL_1:
+ "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
+ by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult zmult_1_right)
+
+lemma dest_int_rep:
+ "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
+ by (metis (full_types) of_int_of_nat real_eq_of_int real_of_nat_def)
+
+lemma DEF_int_add:
+ "op + = (\<lambda>u ua. floor (real u + real ua))"
+ by simp
+
+lemma DEF_int_sub:
+ "op - = (\<lambda>u ua. floor (real u - real ua))"
+ by simp
+
+lemma DEF_int_mul:
+ "op * = (\<lambda>u ua. floor (real u * real ua))"
+ by (metis floor_number_of number_of_is_id number_of_real_def real_eq_of_int real_of_int_mult)
+
+lemma DEF_int_abs:
+ "abs = (\<lambda>u. floor (abs (real u)))"
+ by (metis floor_real_of_int real_of_int_abs)
+
+lemma DEF_int_sgn:
+ "sgn = (\<lambda>u. floor (sgn (real u)))"
+ by (simp add: sgn_if fun_eq_iff)
+
+lemma int_sgn_th:
+ "real (sgn (x :: int)) = sgn (real x)"
+ by (simp add: sgn_if)
+
+lemma DEF_int_max:
+ "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
+ by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max zle_linear)
+
+lemma int_max_th:
+ "real (max (x :: int) y) = max (real x) (real y)"
+ by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff zle_linear)
+
+lemma DEF_int_min:
+ "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
+ by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
+
+lemma int_min_th:
+ "real (min (x :: int) y) = min (real x) (real y)"
+ by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
+
+lemma INT_IMAGE:
+ "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
+ by (metis number_of_eq number_of_is_id of_int_of_nat)
+
+lemma DEF_int_pow:
+ "op ^ = (\<lambda>u ua. floor (real u ^ ua))"
+ by (simp add: floor_power)
+
+lemma DEF_int_divides:
+ "op dvd = (\<lambda>(u :: int) ua. \<exists>x. ua = u * x)"
+ by (metis dvdE dvdI)
+
+lemma DEF_int_divides':
+ "(a :: int) dvd b = (\<exists>x. b = a * x)"
+ by (metis dvdE dvdI)
+
+definition "int_mod (u :: int) ua ub = (u dvd (ua - ub))"
+
+lemma int_mod_def':
+ "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
+ by (simp add: int_mod_def_raw)
+
+lemma int_congruent:
+ "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
+ unfolding int_mod_def'
+ by (auto simp add: DEF_int_divides')
+
+lemma int_congruent':
+ "\<forall>(x :: int) y n. (n dvd x - y) = (\<exists>d. x - y = n * d)"
+ using int_congruent[unfolded int_mod_def] .
+
+fun int_gcd where
+ "int_gcd ((a :: int), (b :: int)) = gcd a b"
+
+definition "hl_mod (k\<Colon>int) (l\<Colon>int) = (if 0 \<le> l then k mod l else k mod - l)"
+
+lemma hl_mod_nonneg:
+ "b \<noteq> 0 \<Longrightarrow> hl_mod a b \<ge> 0"
+ by (simp add: hl_mod_def)
+
+lemma hl_mod_lt_abs:
+ "b \<noteq> 0 \<Longrightarrow> hl_mod a b < abs b"
+ by (simp add: hl_mod_def)
+
+definition "hl_div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
+
+lemma hl_mod_div:
+ "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
+ unfolding hl_div_def hl_mod_def
+ by auto (metis zmod_zdiv_equality zmult_commute zmult_zminus)
+
+lemma sth:
+ "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
+ (\<forall>(x :: int) y. x + y = y + x) \<and>
+ (\<forall>(x :: int). int 0 + x = x) \<and>
+ (\<forall>(x :: int) y z. x * (y * z) = x * y * z) \<and>
+ (\<forall>(x :: int) y. x * y = y * x) \<and>
+ (\<forall>(x :: int). int 1 * x = x) \<and>
+ (\<forall>(x :: int). int 0 * x = int 0) \<and>
+ (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
+ (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
+ by (simp_all add: zadd_zmult_distrib2)
+
+lemma INT_DIVISION:
+ "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"
+ by (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+
+lemma INT_DIVMOD_EXIST_0:
+ "\<exists>q r. if n = int 0 then q = int 0 \<and> r = m
+ else int 0 \<le> r \<and> r < abs n \<and> m = q * n + r"
+ apply (rule_tac x="hl_div m n" in exI)
+ apply (rule_tac x="hl_mod m n" in exI)
+ apply (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+ unfolding hl_div_def hl_mod_def
+ by auto
+
+lemma DEF_div:
+ "hl_div = (SOME q. \<exists>r. \<forall>m n. if n = int 0 then q m n = int 0 \<and> r m n = m
+ else (int 0) \<le> (r m n) \<and> (r m n) < (abs n) \<and> m = ((q m n) * n) + (r m n))"
+ apply (rule some_equality[symmetric])
+ apply (rule_tac x="hl_mod" in exI)
+ apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+ apply (simp add: hl_div_def)
+ apply (simp add: hl_mod_def)
+ apply (drule_tac x="x" in spec)
+ apply (drule_tac x="xa" in spec)
+ apply (case_tac "0 = xa")
+ apply (simp add: hl_mod_def hl_div_def)
+ apply (case_tac "xa > 0")
+ apply (simp add: hl_mod_def hl_div_def)
+ 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)
+ apply (simp add: hl_mod_def hl_div_def)
+ 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)
+
+lemma DEF_rem:
+ "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
+ (if 0 \<le> n then m div n else - (m div - n)) = int 0 \<and> r m n = m
+ else int 0 \<le> r m n \<and> r m n < abs n \<and>
+ m = (if 0 \<le> n then m div n else - (m div - n)) * n + r m n)"
+ apply (rule some_equality[symmetric])
+ apply (fold hl_div_def)
+ apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
+ apply (simp add: hl_div_def)
+ apply (simp add: hl_mod_def)
+ apply (drule_tac x="x" in spec)
+ apply (drule_tac x="xa" in spec)
+ apply (case_tac "0 = xa")
+ apply (simp add: hl_mod_def hl_div_def)
+ apply (case_tac "xa > 0")
+ apply (simp add: hl_mod_def hl_div_def)
+ apply (metis add_left_cancel mod_div_equality)
+ apply (simp add: hl_mod_def hl_div_def)
+ by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial zadd_commute zminus_zmod zmod_zminus2 zmult_commute)
+
+lemma DEF_int_gcd:
+ "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
+ (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
+ apply (rule some_equality[symmetric])
+ apply auto
+ apply (metis bezout_int zmult_commute)
+ apply (auto simp add: fun_eq_iff)
+ apply (drule_tac x="a" in spec)
+ apply (drule_tac x="b" in spec)
+ using gcd_greatest_int zdvd_antisym_nonneg
+ by auto
+
+definition "eqeq x y (r :: 'a \<Rightarrow> 'b \<Rightarrow> bool) = r x y"
+
+lemma INT_INTEGRAL:
+ "(\<forall>x. int 0 * x = int 0) \<and>
+ (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and>
+ (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))"
+ by (auto simp add: crossproduct_eq)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOLLightList.thy Wed Jul 13 00:23:24 2011 +0900
@@ -0,0 +1,332 @@
+(* Title: HOL/Import/HOLLightList.thy
+ Author: Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light lists *}
+
+theory HOLLightList
+imports List
+begin
+
+lemma AND_ALL2:
+ "(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"
+ by (induct l m rule: list_induct2') auto
+
+lemma MEM_EXISTS_EL:
+ "(x \<in> set l) = (\<exists>i<length l. x = l ! i)"
+ by (auto simp add: in_set_conv_nth)
+
+lemma INJECTIVE_MAP:
+ "(\<forall>l m. map f l = map f m --> l = m) = (\<forall>x y. f x = f y --> x = y)"
+proof (intro iffI allI impI)
+ fix x y
+ assume "\<forall>l m. map f l = map f m \<longrightarrow> l = m" "f x = f y"
+ then show "x = y"
+ by (drule_tac x="[x]" in spec) (drule_tac x="[y]" in spec, simp)
+next
+ fix l m
+ assume a: "\<forall>x y. f x = f y \<longrightarrow> x = y"
+ assume "map f l = map f m"
+ then show "l = m"
+ by (induct l m rule: list_induct2') (simp_all add: a)
+qed
+
+lemma SURJECTIVE_MAP:
+ "(\<forall>m. EX l. map f l = m) = (\<forall>y. EX x. f x = y)"
+ apply (intro iffI allI)
+ apply (drule_tac x="[y]" in spec)
+ apply (elim exE)
+ apply (case_tac l)
+ apply simp
+ apply (rule_tac x="a" in exI)
+ apply simp
+ apply (induct_tac m)
+ apply simp
+ apply (drule_tac x="a" in spec)
+ apply (elim exE)
+ apply (rule_tac x="x # l" in exI)
+ apply simp
+ done
+
+lemma LENGTH_TL:
+ "l \<noteq> [] \<longrightarrow> length (tl l) = length l - 1"
+ by simp
+
+lemma DEF_APPEND:
+ "op @ = (SOME APPEND. (\<forall>l. APPEND [] l = l) \<and> (\<forall>h t l. APPEND (h # t) l = h # APPEND t l))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
+lemma DEF_REVERSE:
+ "rev = (SOME REVERSE. REVERSE [] = [] \<and> (\<forall>l x. REVERSE (x # l) = (REVERSE l) @ [x]))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
+lemma DEF_LENGTH:
+ "length = (SOME LENGTH. LENGTH [] = 0 \<and> (\<forall>h t. LENGTH (h # t) = Suc (LENGTH t)))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
+lemma DEF_MAP:
+ "map = (SOME MAP. (\<forall>f. MAP f [] = []) \<and> (\<forall>f h t. MAP f (h # t) = f h # MAP f t))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac xa)
+ apply simp_all
+ done
+
+lemma DEF_REPLICATE:
+ "replicate =
+ (SOME REPLICATE. (\<forall>x. REPLICATE 0 x = []) \<and> (\<forall>n x. REPLICATE (Suc n) x = x # REPLICATE n x))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
+lemma DEF_ITLIST:
+ "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)))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac xa)
+ apply simp_all
+ done
+
+lemma DEF_ALL2: "list_all2 =
+ (SOME ALL2.
+ (\<forall>P l2. ALL2 P [] l2 = (l2 = [])) \<and>
+ (\<forall>h1 P t1 l2.
+ ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \<and> ALL2 P t1 (tl l2))))"
+ apply (rule some_equality[symmetric])
+ apply (auto)
+ apply (case_tac l2, simp_all)
+ apply (case_tac l2, simp_all)
+ apply (case_tac l2, simp_all)
+ apply (simp add: fun_eq_iff)
+ apply (intro allI)
+ apply (induct_tac xa xb rule: list_induct2')
+ apply simp_all
+ done
+
+lemma ALL2:
+ "list_all2 P [] [] = True \<and>
+ list_all2 P (h1 # t1) [] = False \<and>
+ list_all2 P [] (h2 # t2) = False \<and>
+ list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \<and> list_all2 P t1 t2)"
+ by simp
+
+lemma DEF_FILTER:
+ "filter = (SOME FILTER. (\<forall>P. FILTER P [] = []) \<and>
+ (\<forall>h P t. FILTER P (h # t) = (if P h then h # FILTER P t else FILTER P t)))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac xa)
+ apply simp_all
+ done
+
+fun map2 where
+ "map2 f [] [] = []"
+| "map2 f (h1 # t1) (h2 # t2) = (f h1 h2) # (map2 f t1 t2)"
+
+lemma MAP2:
+ "map2 f [] [] = [] \<and> map2 f (h1 # t1) (h2 # t2) = f h1 h2 # map2 f t1 t2"
+ by simp
+
+fun fold2 where
+ "fold2 f [] [] b = b"
+| "fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
+
+lemma ITLIST2:
+ "fold2 f [] [] b = b \<and> fold2 f (h1 # t1) (h2 # t2) b = f h1 h2 (fold2 f t1 t2 b)"
+ by simp
+
+definition [simp]: "list_el x xs = nth xs x"
+
+lemma ZIP:
+ "zip [] [] = [] \<and> zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)"
+ by simp
+
+lemma LAST_CLAUSES:
+ "last [h] = h \<and> last (h # k # t) = last (k # t)"
+ by simp
+
+lemma DEF_NULL:
+ "List.null = (SOME NULL. NULL [] = True \<and> (\<forall>h t. NULL (h # t) = False))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: fun_eq_iff null_def)
+ apply (case_tac x)
+ apply simp_all
+ done
+
+lemma DEF_ALL:
+ "list_all = (SOME u. (\<forall>P. u P [] = True) \<and> (\<forall>h P t. u P (h # t) = (P h \<and> u P t)))"
+ apply (rule some_equality[symmetric])
+ apply auto[1]
+ apply (simp add: fun_eq_iff)
+ apply (intro allI)
+ apply (induct_tac xa)
+ apply simp_all
+ done
+
+lemma MAP_EQ:
+ "list_all (\<lambda>x. f x = g x) l \<longrightarrow> map f l = map g l"
+ by (induct l) auto
+
+definition [simp]: "list_mem x xs = List.member xs x"
+
+lemma DEF_MEM:
+ "list_mem = (SOME MEM. (\<forall>x. MEM x [] = False) \<and> (\<forall>h x t. MEM x (h # t) = (x = h \<or> MEM x t)))"
+ apply (rule some_equality[symmetric])
+ apply (auto simp add: member_def)[1]
+ apply (simp add: fun_eq_iff)
+ apply (intro allI)
+ apply (induct_tac xa)
+ apply (simp_all add: member_def)
+ done
+
+lemma DEF_EX:
+ "list_ex = (SOME u. (\<forall>P. u P [] = False) \<and> (\<forall>h P t. u P (h # t) = (P h \<or> u P t)))"
+ apply (rule some_equality[symmetric])
+ apply (auto)
+ apply (simp add: fun_eq_iff)
+ apply (intro allI)
+ apply (induct_tac xa)
+ apply (simp_all)
+ done
+
+lemma ALL_IMP:
+ "(\<forall>x. x \<in> set l \<and> P x \<longrightarrow> Q x) \<and> list_all P l \<longrightarrow> list_all Q l"
+ by (simp add: list_all_iff)
+
+lemma NOT_EX: "(\<not> list_ex P l) = list_all (\<lambda>x. \<not> P x) l"
+ by (simp add: list_all_iff list_ex_iff)
+
+lemma NOT_ALL: "(\<not> list_all P l) = list_ex (\<lambda>x. \<not> P x) l"
+ by (simp add: list_all_iff list_ex_iff)
+
+lemma ALL_MAP: "list_all P (map f l) = list_all (P o f) l"
+ by (simp add: list_all_iff)
+
+lemma ALL_T: "list_all (\<lambda>x. True) l"
+ by (simp add: list_all_iff)
+
+lemma MAP_EQ_ALL2: "list_all2 (\<lambda>x y. f x = f y) l m \<longrightarrow> map f l = map f m"
+ by (induct l m rule: list_induct2') simp_all
+
+lemma ALL2_MAP: "list_all2 P (map f l) l = list_all (\<lambda>a. P (f a) a) l"
+ by (induct l) simp_all
+
+lemma MAP_EQ_DEGEN: "list_all (\<lambda>x. f x = x) l --> map f l = l"
+ by (induct l) simp_all
+
+lemma ALL2_AND_RIGHT:
+ "list_all2 (\<lambda>x y. P x \<and> Q x y) l m = (list_all P l \<and> list_all2 Q l m)"
+ by (induct l m rule: list_induct2') auto
+
+lemma ITLIST_EXTRA:
+ "foldr f (l @ [a]) b = foldr f l (f a b)"
+ by simp
+
+lemma ALL_MP:
+ "list_all (\<lambda>x. P x \<longrightarrow> Q x) l \<and> list_all P l \<longrightarrow> list_all Q l"
+ by (simp add: list_all_iff)
+
+lemma AND_ALL:
+ "(list_all P l \<and> list_all Q l) = list_all (\<lambda>x. P x \<and> Q x) l"
+ by (auto simp add: list_all_iff)
+
+lemma EX_IMP:
+ "(\<forall>x. x\<in>set l \<and> P x \<longrightarrow> Q x) \<and> list_ex P l \<longrightarrow> list_ex Q l"
+ by (auto simp add: list_ex_iff)
+
+lemma ALL_MEM:
+ "(\<forall>x. x\<in>set l \<longrightarrow> P x) = list_all P l"
+ by (auto simp add: list_all_iff)
+
+lemma EX_MAP:
+ "ALL P f l. list_ex P (map f l) = list_ex (P o f) l"
+ by (simp add: list_ex_iff)
+
+lemma EXISTS_EX:
+ "\<forall>P l. (EX x. list_ex (P x) l) = list_ex (\<lambda>s. EX x. P x s) l"
+ by (auto simp add: list_ex_iff)
+
+lemma FORALL_ALL:
+ "\<forall>P l. (\<forall>x. list_all (P x) l) = list_all (\<lambda>s. \<forall>x. P x s) l"
+ by (auto simp add: list_all_iff)
+
+lemma MEM_APPEND: "\<forall>x l1 l2. (x\<in>set (l1 @ l2)) = (x\<in>set l1 \<or> x\<in>set l2)"
+ by simp
+
+lemma MEM_MAP: "\<forall>f y l. (y\<in>set (map f l)) = (EX x. x\<in>set l \<and> y = f x)"
+ by auto
+
+lemma MEM_FILTER: "\<forall>P l x. (x\<in>set (filter P l)) = (P x \<and> x\<in>set l)"
+ by auto
+
+lemma EX_MEM: "(EX x. P x \<and> x\<in>set l) = list_ex P l"
+ by (auto simp add: list_ex_iff)
+
+lemma ALL2_MAP2:
+ "list_all2 P (map f l) (map g m) = list_all2 (\<lambda>x y. P (f x) (g y)) l m"
+ by (simp add: list_all2_map1 list_all2_map2)
+
+lemma ALL2_ALL:
+ "list_all2 P l l = list_all (\<lambda>x. P x x) l"
+ by (induct l) simp_all
+
+lemma LENGTH_MAP2:
+ "length l = length m \<longrightarrow> length (map2 f l m) = length m"
+ by (induct l m rule: list_induct2') simp_all
+
+lemma DEF_set_of_list:
+ "set = (SOME sol. sol [] = {} \<and> (\<forall>h t. sol (h # t) = insert h (sol t)))"
+ apply (rule some_equality[symmetric])
+ apply (simp_all)
+ apply (rule ext)
+ apply (induct_tac x)
+ apply simp_all
+ done
+
+lemma IN_SET_OF_LIST:
+ "ALL x l. (x\<in>set l) = list_mem x l"
+ by (simp add: member_def)
+
+lemma DEF_BUTLAST:
+ "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"
+ apply (rule some_equality[symmetric])
+ apply auto
+ apply (rule ext)
+ apply (induct_tac x)
+ apply auto
+ done
+
+lemma MONO_ALL:
+ "(ALL x. P x \<longrightarrow> Q x) \<longrightarrow> list_all P l \<longrightarrow> list_all Q l"
+ by (simp add: list_all_iff)
+
+lemma EL_TL: "l \<noteq> [] \<Longrightarrow> tl l ! x = l ! (x + 1)"
+ by (induct l) (simp_all)
+
+(* Assume the same behaviour outside of the usual domain.
+ For HD, LAST, EL it follows from "undefined = SOME _. False".
+
+ The definitions of TL and ZIP are different for empty lists.
+ *)
+axioms
+ DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
+ DEF_LAST: "last =
+ (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
+ DEF_EL: "list_el =
+ (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOLLightReal.thy Wed Jul 13 00:23:24 2011 +0900
@@ -0,0 +1,331 @@
+(* Title: HOL/Import/HOLLightReal.thy
+ Author: Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light reals *}
+
+theory HOLLightReal imports Real begin
+
+lemma REAL_OF_NUM_MAX:
+ "max (real (m :: nat)) (real n) = real (max m n)"
+ by simp
+
+lemma REAL_OF_NUM_MIN:
+ "min (real (m :: nat)) (real n) = real (min m n)"
+ by simp
+
+lemma REAL_POLY_NEG_CLAUSES:
+ "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
+ by simp
+
+lemma REAL_MUL_AC:
+ "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
+ by simp
+
+lemma REAL_EQ_ADD_LCANCEL_0:
+ "((x :: real) + y = x) = (y = 0)"
+ by simp
+
+lemma REAL_EQ_ADD_RCANCEL_0:
+ "((x :: real) + y = y) = (x = 0)"
+ by simp
+
+lemma REAL_LT_ANTISYM:
+ "\<not> ((x :: real) < y \<and> y < x)"
+ by simp
+
+lemma REAL_LET_ANTISYM:
+ "\<not> ((x :: real) \<le> y \<and> y < x)"
+ by simp
+
+lemma REAL_LT_NEGTOTAL:
+ "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
+ by auto
+
+lemma REAL_LT_ADDNEG:
+ "((y :: real) < x + - z) = (y + z < x)"
+ by auto
+
+lemma REAL_LT_ADDNEG2:
+ "((x :: real) + - y < z) = (x < z + y)"
+ by auto
+
+lemma REAL_LT_ADD1:
+ "(x :: real) \<le> y \<longrightarrow> x < y + 1"
+ by simp
+
+lemma REAL_SUB_ADD2:
+ "(y :: real) + (x - y) = x"
+ by simp
+
+lemma REAL_ADD_SUB:
+ "(x :: real) + y - x = y"
+ by simp
+
+lemma REAL_NEG_EQ:
+ "(- (x :: real) = y) = (x = - y)"
+ by auto
+
+lemma REAL_LE_ADDR:
+ "((x :: real) \<le> x + y) = (0 \<le> y)"
+ by simp
+
+lemma REAL_LE_ADDL:
+ "((y :: real) \<le> x + y) = (0 \<le> x)"
+ by simp
+
+lemma REAL_LT_ADDR:
+ "((x :: real) < x + y) = (0 < y)"
+ by simp
+
+lemma REAL_LT_ADDL:
+ "((y :: real) < x + y) = (0 < x)"
+ by simp
+
+lemma REAL_SUB_SUB:
+ "(x :: real) - y - x = - y"
+ by simp
+
+lemma REAL_SUB_LNEG:
+ "- (x :: real) - y = - (x + y)"
+ by simp
+
+lemma REAL_SUB_NEG2:
+ "- (x :: real) - - y = y - x"
+ by simp
+
+lemma REAL_SUB_TRIANGLE:
+ "(a :: real) - b + (b - c) = a - c"
+ by simp
+
+lemma REAL_SUB_SUB2:
+ "(x :: real) - (x - y) = y"
+ by simp
+
+lemma REAL_ADD_SUB2:
+ "(x :: real) - (x + y) = - y"
+ by simp
+
+lemma REAL_POS_NZ:
+ "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+ by simp
+
+lemma REAL_DIFFSQ:
+ "((x :: real) + y) * (x - y) = x * x - y * y"
+ by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
+
+lemma REAL_ABS_TRIANGLE_LE:
+ "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
+ by auto
+
+lemma REAL_ABS_TRIANGLE_LT:
+ "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
+ by auto
+
+lemma REAL_ABS_REFL:
+ "(abs (x :: real) = x) = (0 \<le> x)"
+ by auto
+
+lemma REAL_ABS_BETWEEN:
+ "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
+ by auto
+
+lemma REAL_ABS_BOUND:
+ "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
+ by auto
+
+lemma REAL_ABS_STILLNZ:
+ "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
+ by auto
+
+lemma REAL_ABS_CASES:
+ "(x :: real) = 0 \<or> 0 < abs x"
+ by simp
+
+lemma REAL_ABS_BETWEEN1:
+ "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
+ by auto
+
+lemma REAL_ABS_SIGN:
+ "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
+ by auto
+
+lemma REAL_ABS_SIGN2:
+ "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
+ by auto
+
+lemma REAL_ABS_CIRCLE:
+ "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
+ by auto
+
+lemma REAL_BOUNDS_LT:
+ "(- (k :: real) < x \<and> x < k) = (abs x < k)"
+ by auto
+
+lemma REAL_MIN_MAX:
+ "min (x :: real) y = - max (- x) (- y)"
+ by auto
+
+lemma REAL_MAX_MIN:
+ "max (x :: real) y = - min (- x) (- y)"
+ by auto
+
+lemma REAL_MAX_MAX:
+ "(x :: real) \<le> max x y \<and> y \<le> max x y"
+ by simp
+
+lemma REAL_MIN_MIN:
+ "min (x :: real) y \<le> x \<and> min x y \<le> y"
+ by simp
+
+lemma REAL_MAX_ACI:
+ "max (x :: real) y = max y x \<and>
+ max (max x y) z = max x (max y z) \<and>
+ max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
+ by auto
+
+
+lemma REAL_MIN_ACI:
+ "min (x :: real) y = min y x \<and>
+ min (min x y) z = min x (min y z) \<and>
+ min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
+ by auto
+
+lemma REAL_EQ_MUL_RCANCEL:
+ "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
+ by auto
+
+lemma REAL_MUL_LINV_UNIQ:
+ "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
+ by (metis inverse_inverse_eq inverse_unique)
+
+lemma REAL_DIV_RMUL:
+ "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
+ by simp
+
+lemma REAL_DIV_LMUL:
+ "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
+ by simp
+
+lemma REAL_LT_IMP_NZ:
+ "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+ by simp
+
+lemma REAL_LT_LCANCEL_IMP:
+ "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
+ by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_LT_RCANCEL_IMP:
+ "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
+ by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_MUL_POS_LE:
+ "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
+ by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
+
+lemma REAL_EQ_RDIV_EQ:
+ "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
+ by auto
+
+lemma REAL_EQ_LDIV_EQ:
+ "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
+ by auto
+
+lemma REAL_SUB_INV:
+ "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
+ by (simp add: division_ring_inverse_diff real_divide_def)
+
+lemma REAL_DOWN:
+ "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
+ by (intro impI exI[of _ "d / 2"]) simp
+
+lemma REAL_POW_MONO_LT:
+ "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
+ by simp
+
+lemma REAL_POW_MONO:
+ "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
+ by (cases "m < n", cases "x = 1") auto
+
+lemma REAL_EQ_LCANCEL_IMP:
+ "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
+ by auto
+
+lemma REAL_LE_DIV:
+ "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
+ by (simp add: zero_le_divide_iff)
+
+lemma REAL_10: "(1::real) \<noteq> 0"
+ by simp
+
+lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
+ by simp
+
+lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
+ by simp
+
+lemma REAL_ADD_LINV: "-x + x = (0::real)"
+ by simp
+
+lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
+ by simp
+
+lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
+ by auto
+
+lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
+ by auto
+
+lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
+ by (simp add: real_of_nat_Suc)
+
+lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
+ by (simp add: abs_if)
+
+lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
+ by simp
+
+lemma REAL_POLY_CLAUSES:
+ "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
+ (\<forall>(x :: real) y. x + y = y + x) \<and>
+ (\<forall>(x :: real). 0 + x = x) \<and>
+ (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
+ (\<forall>(x :: real) y. x * y = y * x) \<and>
+ (\<forall>(x :: real). 1 * x = x) \<and>
+ (\<forall>(x :: real). 0 * x = 0) \<and>
+ (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
+ (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
+ by (auto simp add: mult.add_right)
+
+lemma REAL_COMPLETE:
+ "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+ (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+ (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+ apply (intro allI impI, elim conjE)
+ apply (drule complete_real[unfolded Ball_def mem_def])
+ apply simp_all
+ done
+
+lemma REAL_COMPLETE_SOMEPOS:
+ "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+ (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+ (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+ using REAL_COMPLETE by auto
+
+lemma REAL_ADD_AC:
+ "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
+ by simp
+
+lemma REAL_LE_RNEG:
+ "((x :: real) \<le> - y) = (x + y \<le> 0)"
+ by auto
+
+lemma REAL_LE_NEGTOTAL:
+ "0 \<le> (x :: real) \<or> 0 \<le> - x"
+ by auto
+
+lemma DEF_real_sgn:
+ "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
+ by (simp add: ext)
+
+end
--- a/src/HOL/Import/hol4rews.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/HOL/Import/hol4rews.ML Wed Jul 13 00:23:24 2011 +0900
@@ -160,13 +160,16 @@
let
val _ = message "Adding HOL4 rewrite"
val th1 = th RS @{thm eq_reflection}
+ handle _ => th
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
in
(Context.Theory updated_thy,th1)
end
- | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
+ | add_hol4_rewrite (context, th) = (context,
+ (th RS @{thm eq_reflection} handle _ => th)
+ );
fun ignore_hol4 bthy bthm thy =
let
--- a/src/HOL/Import/import_syntax.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/HOL/Import/import_syntax.ML Wed Jul 13 00:23:24 2011 +0900
@@ -58,7 +58,7 @@
let
val _ = ImportRecorder.load_history thyname
val thy = Replay.import_thms thyname int_thms thmnames thy
- handle x => (ImportRecorder.save_history thyname; raise x) (* FIXME avoid handle x ?? *)
+ (*handle x => (ImportRecorder.save_history thyname; raise x)*) (* FIXME avoid handle x ?? *)
val _ = ImportRecorder.save_history thyname
val _ = ImportRecorder.clear_history ()
in
--- a/src/HOL/Import/proof_kernel.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/HOL/Import/proof_kernel.ML Wed Jul 13 00:23:24 2011 +0900
@@ -187,60 +187,63 @@
fun quotename c =
if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
-fun simple_smart_string_of_cterm ctxt0 ct =
- let
- val ctxt = ctxt0
- |> Config.put show_brackets false
- |> Config.put show_all_types true
- |> Config.put show_sorts true
- |> Config.put Syntax.ambiguity_enabled true;
- val {t,T,...} = rep_cterm ct
- (* Hack to avoid parse errors with Trueprop *)
- val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
- handle TERM _ => ct
- in
- quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
- end
+exception SMART_STRING
-exception SMART_STRING
+fun no_vars context tm =
+ let
+ val ctxt = Variable.set_body false context;
+ val ([tm'], _) = Variable.import_terms true [tm] ctxt;
+ in tm' end
fun smart_string_of_cterm ctxt0 ct =
let
- val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
+ val ctxt = ctxt0
+ |> Config.put Syntax.ambiguity_enabled true
+ |> Config.put show_brackets false
+ |> Config.put show_all_types false
+ |> Config.put show_types false
+ |> Config.put show_sorts false;
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
- val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
- handle TERM _ => ct
- fun match u = t aconv u
- fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
- | G 1 f ctxt x = G 0 f (Config.put show_brackets true ctxt) x
- | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
- | G 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
+ val t' = HOLogic.dest_Trueprop t
+ handle TERM _ => t
+ val tn = no_vars ctxt t'
+ fun match u =
+ let val _ = Thm.match (ct, cterm_of (Proof_Context.theory_of ctxt) u) in true end
+ handle MATCH => false
+ fun G 0 f ctxt x = f ctxt x
+ | G 1 f ctxt x = f (Config.put show_types true ctxt) x
+ | G 2 f ctxt x = G 1 f (Config.put show_sorts true ctxt) x
+ | G 3 f ctxt x = G 2 f (Config.put show_all_types true ctxt) x
+ | G 4 f ctxt x = G 3 f (Config.put show_brackets true ctxt) x
| G _ _ _ _ = raise SMART_STRING
fun F n =
let
- val str =
- G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
+ val str = G n Syntax.string_of_term ctxt tn
+ val _ = warning (PolyML.makestring (n, str))
val u = Syntax.parse_term ctxt str
- |> Type.constraint T |> Syntax.check_term ctxt
+ val u = if t = t' then u else HOLogic.mk_Trueprop u
+ val u = Syntax.check_term ctxt (Type.constraint T u)
in
if match u
then quote str
else F (n+1)
end
- handle ERROR mesg => F (n + 1)
+ handle ERROR _ => F (n + 1)
| SMART_STRING =>
- error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
+ let val _ =
+ warning ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
+ in quote (G 2 Syntax.string_of_term ctxt tn) end
in
Print_Mode.setmp [] F 0
end
- handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
+val topctxt = ML_Context.the_local_context ();
fun prin t = writeln (Print_Mode.setmp []
- (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
+ (fn () => Syntax.string_of_term topctxt t) ());
fun pth (HOLThm(ren,thm)) =
let
(*val _ = writeln "Renaming:"
@@ -1363,6 +1366,7 @@
val thy' = add_hol4_pending thyname thmname args thy
val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val th = disambiguate_frees th
+ val th = Object_Logic.rulify th
val thy2 =
if gen_output
then