# HG changeset patch # User Cezary Kaliszyk # Date 1310484204 -32400 # Node ID 2bd54d4b5f3dccbf7672d6e6286e4701b93c3faa # Parent 9545bb3cefac21c6529eec51bbe98798db306359 HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems diff -r 9545bb3cefac -r 2bd54d4b5f3d src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- 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 \ nat \ nat" - "*" > Groups.times :: "nat \ nat \ nat" - "-" > Groups.minus :: "nat \ nat \ nat" + NUMERAL > HOLLightCompat.NUMERAL + mk_num > Fun.id + "+" > Groups.plus_class.plus :: "nat \ nat \ nat" + "*" > Groups.times_class.times :: "nat \ nat \ nat" + "-" > Groups.minus_class.minus :: "nat \ nat \ nat" + "<" > Orderings.ord_class.less :: "nat \ nat \ bool" + "<=" > Orderings.ord_class.less_eq :: "nat \ nat \ bool" + ">" > Orderings.ord_class.greater :: "nat \ nat \ bool" + ">=" > Orderings.ord_class.greater_eq :: "nat \ nat \ bool" + EXP > Power.power_class.power :: "nat \ nat \ nat" + MAX > Orderings.ord_class.max :: "nat \ nat \ nat" + MIN > Orderings.ord_class.min :: "nat \ nat \ nat" + DIV > Divides.div_class.div :: "nat \ nat \ nat" + MOD > Divides.div_class.mod :: "nat \ nat \ 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 \ bool" + ODD > HOLLightCompat.ODD + FACT > Fact.fact_class.fact :: "nat \ 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 \ bool" + GABS > Hilbert_Choice.Eps + GEQ > HOL.eq + GSPEC > Set.Collect + SETSPEC > HOLLightCompat.SETSPEC + UNION > Lattices.semilattice_sup_class.sup :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" + UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \ bool) \ bool) \ 'a \ bool" + INTER > Lattices.semilattice_inf_class.inf :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" + INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \ bool) \ bool) \ 'a \ bool" + DIFF > Groups.minus_class.minus :: "('a \ bool) \ ('a \ bool) \ 'a \ bool" + SUBSET > Orderings.ord_class.less_eq :: "('a \ bool) \ ('a \ bool) \ bool" + PSUBSET > Orderings.ord_class.less :: "('a \ bool) \ ('a \ bool) \ 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 \ 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 \ real \ bool" + real_le > Orderings.ord_class.less_eq :: "real \ real \ bool" + real_gt > Orderings.ord_class.greater :: "real \ real \ bool" + real_ge > Orderings.ord_class.greater_eq :: "real \ real \ bool" + real_pow > Power.power_class.power :: "real \ nat \ real" + real_abs > Groups.abs_class.abs :: "real \ real" + real_max > Orderings.ord_class.max :: "real \ real \ real" + real_min > Orderings.ord_class.min :: "real \ real \ real" + real_sgn > Groups.sgn_class.sgn :: "real \ real"*) +(*real_of_int > RealDef.real :: "int => real" + int_of_real > Archimedean_Field.floor :: "real \ int" + dest_int > RealDef.real :: "int => real" + mk_int > Archimedean_Field.floor :: "real \ int" + int_lt > Orderings.ord_class.less :: "int \ int \ bool" + int_le > Orderings.ord_class.less_eq :: "int \ int \ bool" + int_gt > Orderings.ord_class.greater :: "int \ int \ bool" + int_ge > Orderings.ord_class.greater_eq :: "int \ int \ bool" + int_of_num > Nat.semiring_1_class.of_nat :: "nat \ int" + int_neg > Groups.uminus_class.uminus :: "int \ 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 \ int" + int_max > Orderings.ord_class.max :: "int \ int \ int" + int_min > Orderings.ord_class.min :: "int \ int \ int" + int_sgn > Groups.sgn_class.sgn :: "int \ int" + int_pow > Power.power_class.power :: "int \ nat \ int" + int_div > HOLLightInt.hl_div :: "int \ int \ int" + div > HOLLightInt.hl_div :: "int \ int \ int" + mod_int > HOLLightInt.hl_mod :: "int \ int \ int" + rem > HOLLightInt.hl_mod :: "int \ int \ int" + int_divides > Rings.dvd_class.dvd :: "int \ int \ bool" + int_mod > HOLLightInt.int_mod :: "int \ int \ int \ bool" + int_gcd > HOLLightInt.int_gcd :: "int \ int \ int" + int_coprime > HOLLightInt.int_coprime :: "int \ int \ 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 diff -r 9545bb3cefac -r 2bd54d4b5f3d src/HOL/Import/HOLLightInt.thy --- /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 = (\u. \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: + "(\n. P (int n)) = (\i\(int 0). P i)" + by (auto, drule_tac x="nat i" in spec) simp + +lemma INT_LT_DISCRETE: + "(x < y) = (x + int 1 \ y)" + by auto + +lemma INT_ABS_MUL_1: + "(abs (x * y) = int 1) = (abs x = int 1 \ 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: + "\(n :: nat). real (i :: int) = real n \ 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 + = (\u ua. floor (real u + real ua))" + by simp + +lemma DEF_int_sub: + "op - = (\u ua. floor (real u - real ua))" + by simp + +lemma DEF_int_mul: + "op * = (\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 = (\u. floor (abs (real u)))" + by (metis floor_real_of_int real_of_int_abs) + +lemma DEF_int_sgn: + "sgn = (\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 = (\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 = (\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: + "(\n. x = int n) \ (\n. x = - int n)" + by (metis number_of_eq number_of_is_id of_int_of_nat) + +lemma DEF_int_pow: + "op ^ = (\u ua. floor (real u ^ ua))" + by (simp add: floor_power) + +lemma DEF_int_divides: + "op dvd = (\(u :: int) ua. \x. ua = u * x)" + by (metis dvdE dvdI) + +lemma DEF_int_divides': + "(a :: int) dvd b = (\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 = (\u ua ub. (u dvd (ua - ub)))" + by (simp add: int_mod_def_raw) + +lemma int_congruent: + "\x xa xb. int_mod xb x xa = (\d. x - xa = xb * d)" + unfolding int_mod_def' + by (auto simp add: DEF_int_divides') + +lemma int_congruent': + "\(x :: int) y n. (n dvd x - y) = (\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\int) (l\int) = (if 0 \ l then k mod l else k mod - l)" + +lemma hl_mod_nonneg: + "b \ 0 \ hl_mod a b \ 0" + by (simp add: hl_mod_def) + +lemma hl_mod_lt_abs: + "b \ 0 \ hl_mod a b < abs b" + by (simp add: hl_mod_def) + +definition "hl_div k l = (if 0 \ l then k div l else -(k div (-l)))" + +lemma hl_mod_div: + "n \ (0\int) \ 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: + "(\(x :: int) y z. x + (y + z) = x + y + z) \ + (\(x :: int) y. x + y = y + x) \ + (\(x :: int). int 0 + x = x) \ + (\(x :: int) y z. x * (y * z) = x * y * z) \ + (\(x :: int) y. x * y = y * x) \ + (\(x :: int). int 1 * x = x) \ + (\(x :: int). int 0 * x = int 0) \ + (\(x :: int) y z. x * (y + z) = x * y + x * z) \ + (\(x :: int). x ^ 0 = int 1) \ (\(x :: int) n. x ^ Suc n = x * x ^ n)" + by (simp_all add: zadd_zmult_distrib2) + +lemma INT_DIVISION: + "n ~= int 0 \ m = hl_div m n * n + hl_mod m n \ int 0 \ hl_mod m n \ 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: + "\q r. if n = int 0 then q = int 0 \ r = m + else int 0 \ r \ r < abs n \ 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. \r. \m n. if n = int 0 then q m n = int 0 \ r m n = m + else (int 0) \ (r m n) \ (r m n) < (abs n) \ 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. \m n. if n = int 0 then + (if 0 \ n then m div n else - (m div - n)) = int 0 \ r m n = m + else int 0 \ r m n \ r m n < abs n \ + m = (if 0 \ 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. \a b. (int 0) \ (d (a, b)) \ (d (a, b)) dvd a \ + (d (a, b)) dvd b \ (\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 \ 'b \ bool) = r x y" + +lemma INT_INTEGRAL: + "(\x. int 0 * x = int 0) \ + (\(x :: int) y z. (x + y = x + z) = (y = z)) \ + (\(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \ y = z))" + by (auto simp add: crossproduct_eq) + +end diff -r 9545bb3cefac -r 2bd54d4b5f3d src/HOL/Import/HOLLightList.thy --- /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 \ list_all2 Q l m) = list_all2 (\x y. P x y \ Q x y) l m" + by (induct l m rule: list_induct2') auto + +lemma MEM_EXISTS_EL: + "(x \ set l) = (\il m. map f l = map f m --> l = m) = (\x y. f x = f y --> x = y)" +proof (intro iffI allI impI) + fix x y + assume "\l m. map f l = map f m \ 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: "\x y. f x = f y \ 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: + "(\m. EX l. map f l = m) = (\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 \ [] \ length (tl l) = length l - 1" + by simp + +lemma DEF_APPEND: + "op @ = (SOME APPEND. (\l. APPEND [] l = l) \ (\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 [] = [] \ (\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 \ (\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. (\f. MAP f [] = []) \ (\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. (\x. REPLICATE 0 x = []) \ (\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. (\f b. ITLIST f [] b = b) \ (\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. + (\P l2. ALL2 P [] l2 = (l2 = [])) \ + (\h1 P t1 l2. + ALL2 P (h1 # t1) l2 = (if l2 = [] then False else P h1 (hd l2) \ 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 \ + list_all2 P (h1 # t1) [] = False \ + list_all2 P [] (h2 # t2) = False \ + list_all2 P (h1 # t1) (h2 # t2) = (P h1 h2 \ list_all2 P t1 t2)" + by simp + +lemma DEF_FILTER: + "filter = (SOME FILTER. (\P. FILTER P [] = []) \ + (\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 [] [] = [] \ 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 \ 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 [] [] = [] \ zip (h1 # t1) (h2 # t2) = (h1, h2) # (zip t1 t2)" + by simp + +lemma LAST_CLAUSES: + "last [h] = h \ last (h # k # t) = last (k # t)" + by simp + +lemma DEF_NULL: + "List.null = (SOME NULL. NULL [] = True \ (\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. (\P. u P [] = True) \ (\h P t. u P (h # t) = (P h \ 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 (\x. f x = g x) l \ 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. (\x. MEM x [] = False) \ (\h x t. MEM x (h # t) = (x = h \ 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. (\P. u P [] = False) \ (\h P t. u P (h # t) = (P h \ 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: + "(\x. x \ set l \ P x \ Q x) \ list_all P l \ list_all Q l" + by (simp add: list_all_iff) + +lemma NOT_EX: "(\ list_ex P l) = list_all (\x. \ P x) l" + by (simp add: list_all_iff list_ex_iff) + +lemma NOT_ALL: "(\ list_all P l) = list_ex (\x. \ 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 (\x. True) l" + by (simp add: list_all_iff) + +lemma MAP_EQ_ALL2: "list_all2 (\x y. f x = f y) l m \ 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 (\a. P (f a) a) l" + by (induct l) simp_all + +lemma MAP_EQ_DEGEN: "list_all (\x. f x = x) l --> map f l = l" + by (induct l) simp_all + +lemma ALL2_AND_RIGHT: + "list_all2 (\x y. P x \ Q x y) l m = (list_all P l \ 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 (\x. P x \ Q x) l \ list_all P l \ list_all Q l" + by (simp add: list_all_iff) + +lemma AND_ALL: + "(list_all P l \ list_all Q l) = list_all (\x. P x \ Q x) l" + by (auto simp add: list_all_iff) + +lemma EX_IMP: + "(\x. x\set l \ P x \ Q x) \ list_ex P l \ list_ex Q l" + by (auto simp add: list_ex_iff) + +lemma ALL_MEM: + "(\x. x\set l \ 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: + "\P l. (EX x. list_ex (P x) l) = list_ex (\s. EX x. P x s) l" + by (auto simp add: list_ex_iff) + +lemma FORALL_ALL: + "\P l. (\x. list_all (P x) l) = list_all (\s. \x. P x s) l" + by (auto simp add: list_all_iff) + +lemma MEM_APPEND: "\x l1 l2. (x\set (l1 @ l2)) = (x\set l1 \ x\set l2)" + by simp + +lemma MEM_MAP: "\f y l. (y\set (map f l)) = (EX x. x\set l \ y = f x)" + by auto + +lemma MEM_FILTER: "\P l x. (x\set (filter P l)) = (P x \ x\set l)" + by auto + +lemma EX_MEM: "(EX x. P x \ x\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 (\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 (\x. P x x) l" + by (induct l) simp_all + +lemma LENGTH_MAP2: + "length l = length m \ 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 [] = {} \ (\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\set l) = list_mem x l" + by (simp add: member_def) + +lemma DEF_BUTLAST: + "butlast = (SOME B. B [] = [] \ (\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 \ Q x) \ list_all P l \ list_all Q l" + by (simp add: list_all_iff) + +lemma EL_TL: "l \ [] \ 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. \t h. HD (h # t) = h)" + DEF_LAST: "last = + (SOME LAST. \h t. LAST (h # t) = (if t = [] then h else LAST t))" + DEF_EL: "list_el = + (SOME EL. (\l. EL 0 l = hd l) \ (\n l. EL (Suc n) l = EL n (tl l)))" + +end diff -r 9545bb3cefac -r 2bd54d4b5f3d src/HOL/Import/HOLLightReal.thy --- /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: + "(\(x :: real). - x = - 1 * x) \ (\(x :: real) y. x - y = x + - 1 * y)" + by simp + +lemma REAL_MUL_AC: + "(m :: real) * n = n * m \ m * n * p = m * (n * p) \ 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: + "\ ((x :: real) < y \ y < x)" + by simp + +lemma REAL_LET_ANTISYM: + "\ ((x :: real) \ y \ y < x)" + by simp + +lemma REAL_LT_NEGTOTAL: + "(x :: real) = 0 \ 0 < x \ 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) \ y \ 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) \ x + y) = (0 \ y)" + by simp + +lemma REAL_LE_ADDL: + "((y :: real) \ x + y) = (0 \ 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) \ x \ 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) \ z \ abs y \ z" + by auto + +lemma REAL_ABS_TRIANGLE_LT: + "abs (x :: real) + abs (y - x) < z \ abs y < z" + by auto + +lemma REAL_ABS_REFL: + "(abs (x :: real) = x) = (0 \ x)" + by auto + +lemma REAL_ABS_BETWEEN: + "(0 < (d :: real) \ x - d < y \ y < x + d) = (abs (y - x) < d)" + by auto + +lemma REAL_ABS_BOUND: + "abs ((x :: real) - y) < d \ y < x + d" + by auto + +lemma REAL_ABS_STILLNZ: + "abs ((x :: real) - y) < abs y \ x \ 0" + by auto + +lemma REAL_ABS_CASES: + "(x :: real) = 0 \ 0 < abs x" + by simp + +lemma REAL_ABS_BETWEEN1: + "(x :: real) < z \ abs (y - x) < z - x \ y < z" + by auto + +lemma REAL_ABS_SIGN: + "abs ((x :: real) - y) < y \ 0 < x" + by auto + +lemma REAL_ABS_SIGN2: + "abs ((x :: real) - y) < - y \ x < 0" + by auto + +lemma REAL_ABS_CIRCLE: + "abs (h :: real) < abs y - abs x \ abs (x + h) < abs y" + by auto + +lemma REAL_BOUNDS_LT: + "(- (k :: real) < x \ 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) \ max x y \ y \ max x y" + by simp + +lemma REAL_MIN_MIN: + "min (x :: real) y \ x \ min x y \ y" + by simp + +lemma REAL_MAX_ACI: + "max (x :: real) y = max y x \ + max (max x y) z = max x (max y z) \ + max x (max y z) = max y (max x z) \ max x x = x \ max x (max x y) = max x y" + by auto + + +lemma REAL_MIN_ACI: + "min (x :: real) y = min y x \ + min (min x y) z = min x (min y z) \ + min x (min y z) = min y (min x z) \