# HG changeset patch # User Cezary Kaliszyk # Date 1310485387 -32400 # Node ID 5be84619e4d413876315f09b5378feb00530ae78 # Parent fea3ed6951e3d30aa1ce31598e8189a5250accf7 Update HOLLightCompat diff -r fea3ed6951e3 -r 5be84619e4d4 src/HOL/Import/HOLLightCompat.thy --- a/src/HOL/Import/HOLLightCompat.thy Wed Jul 13 00:29:33 2011 +0900 +++ b/src/HOL/Import/HOLLightCompat.thy Wed Jul 13 00:43:07 2011 +0900 @@ -1,38 +1,139 @@ (* Title: HOL/Import/HOLLightCompat.thy Author: Steven Obua and Sebastian Skalberg, TU Muenchen + Author: Cezary Kaliszyk *) -theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin +theory HOLLightCompat +imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set" + HOLLightList HOLLightReal HOLLightInt HOL4Setup +begin + +(* list *) +lemmas [hol4rew] = list_el_def member_def list_mem_def +(* int *) +lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def +(* real *) +lemma [hol4rew]: + "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2" + by simp_all + +lemma one: + "\v. v = ()" + by simp -lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)" - by auto; +lemma num_Axiom: + "\e f. \!fn. fn 0 = e \ (\n. fn (Suc n) = f (fn n) n)" + apply (intro allI) + apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I) + apply auto + apply (simp add: fun_eq_iff) + apply (intro allI) + apply (induct_tac xa) + apply simp_all + done -lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2" +lemma SUC_INJ: + "\m n. Suc m = Suc n \ m = n" + by auto + +lemma PAIR: + "(fst x, snd x) = x" by simp -lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))" -proof auto - assume a: "(%f. f t1 t2::bool) = (%f. f True True)" - have b: "(%(x::bool) (y::bool). x) = (%x y. x)" .. - with a - have "t1 = True" - by (rule comb_rule) - thus t1 - by simp -next - assume a: "(%f. f t1 t2::bool) = (%f. f True True)" - have b: "(%(x::bool) (y::bool). y) = (%x y. y)" .. - with a - have "t2 = True" - by (rule comb_rule) - thus t2 - by simp -qed +lemma EXISTS_UNIQUE_THM: + "(Ex1 P) = (Ex P & (\x y. P x & P y --> (x = y)))" + by auto + +lemma DEF__star_: + "op * = (SOME mult. (\n. mult 0 n = 0) \ (\m n. mult (Suc m) n = mult m n + n))" + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext)+ + apply (induct_tac x) + apply auto + done + +lemma DEF__slash__backslash_: + "(t1 \ t2) = ((\f. f t1 t2 :: bool) = (\f. f True True))" + unfolding fun_eq_iff + by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \ b)"], simp) + +lemma DEF__lessthan__equal_: + "op \ = (SOME u. (\m. u m 0 = (m = 0)) \ (\m n. u m (Suc n) = (m = Suc n \ u m n)))" + apply (rule some_equality[symmetric]) + apply auto[1] + apply (simp add: fun_eq_iff) + apply (intro allI) + apply (induct_tac xa) + apply auto + done + +lemma DEF__lessthan_: + "op < = (SOME u. (\m. u m 0 = False) \ (\m n. u m (Suc n) = (m = n \ u m n)))" + apply (rule some_equality[symmetric]) + apply auto[1] + apply (simp add: fun_eq_iff) + apply (intro allI) + apply (induct_tac xa) + apply auto + done + +lemma DEF__greaterthan__equal_: + "(op \) = (%u ua. ua \ u)" + by (simp) + +lemma DEF__greaterthan_: + "(op >) = (%u ua. ua < u)" + by (simp) -definition Pred :: "nat \ nat" where - "Pred n \ n - (Suc 0)" +lemma DEF__equal__equal__greaterthan_: + "(t1 \ t2) = ((t1 \ t2) = t1)" + by auto + +lemma DEF_WF: + "wfP = (\u. \P. (\x. P x) \ (\x. P x \ (\y. u y x \ \ P y)))" + unfolding fun_eq_iff + apply (intro allI, rule, intro allI impI, elim exE) + apply (drule_tac wfE_min[to_pred, unfolded mem_def]) + apply assumption + prefer 2 + apply assumption + apply auto[1] + apply (intro wfI_min[to_pred, unfolded mem_def]) + apply (drule_tac x="Q" in spec) + apply auto + apply (rule_tac x="xb" in bexI) + apply (auto simp add: mem_def) + done + +lemma DEF_UNIV: "UNIV = (%x. True)" + by (auto simp add: mem_def) -lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))" +lemma DEF_UNIONS: + "Sup = (\u. {ua. \x. (\ua. ua \ u \ x \ ua) \ ua = x})" + by (simp add: fun_eq_iff Collect_def) + (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D) + +lemma DEF_UNION: + "op \ = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" + by (auto simp add: mem_def fun_eq_iff Collect_def) + +lemma DEF_SUBSET: "op \ = (\u ua. \x. x \ u \ x \ ua)" + by (metis set_rev_mp subsetI) + +lemma DEF_SND: + "snd = (\p. SOME x. EX y. p = (y, x))" + unfolding fun_eq_iff + by (rule someI2) (auto intro: snd_conv[symmetric] someI2) + +definition [simp, hol4rew]: "SETSPEC x P y \ P & x = y" + +lemma DEF_PSUBSET: "op \ = (\u ua. u \ ua & u \ ua)" + by (auto simp add: mem_def fun_eq_iff) + +definition [hol4rew]: "Pred n = n - (Suc 0)" + +lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\n. PRE (Suc n) = n))" apply (rule some_equality[symmetric]) apply (simp add: Pred_def) apply (rule ext) @@ -40,24 +141,198 @@ apply (auto simp add: Pred_def) done -lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def) +lemma DEF_ONE_ONE: + "inj = (\u. \x1 x2. u x1 = u x2 \ x1 = x2)" + by (simp add: inj_on_def) + +definition ODD'[hol4rew]: "(ODD :: nat \ bool) = odd" -lemma REP_ABS_PAIR: "\ x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y" - apply (subst Abs_Prod_inverse) - apply (auto simp add: Prod_def) +lemma DEF_ODD: + "odd = (SOME ODD. ODD 0 = False \ (\n. ODD (Suc n) = (\ ODD n)))" + apply (rule some_equality[symmetric]) + apply simp + unfolding fun_eq_iff + apply (intro allI) + apply (induct_tac x) + apply simp_all done -lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))" - apply (rule ext, rule someI2) - apply (auto intro: fst_conv[symmetric]) +definition [hol4rew, simp]: "NUMERAL (x :: nat) = x" + +lemma DEF_MOD: + "op mod = (SOME r. \m n. if n = (0 :: nat) then m div n = 0 \ + r m n = m else m = m div n * n + r m n \ r m n < n)" + apply (rule some_equality[symmetric]) + apply (auto simp add: fun_eq_iff) + apply (case_tac "xa = 0") + apply auto + apply (drule_tac x="x" in spec) + apply (drule_tac x="xa" in spec) + apply auto + by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute) + +definition "MEASURE = (%u x y. (u x :: nat) < u y)" + +lemma [hol4rew]: + "MEASURE u = (%a b. measure u (a, b))" + unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def + by simp + +definition + "LET f s = f s" + +lemma [hol4rew]: + "LET f s = Let s f" + by (simp add: LET_def Let_def) + +lemma DEF_INTERS: + "Inter = (\u. {ua. \x. (\ua. ua \ u \ x \ ua) \ ua = x})" + by (auto simp add: fun_eq_iff mem_def Collect_def) + (metis InterD InterI mem_def)+ + +lemma DEF_INTER: + "op \ = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" + by (auto simp add: mem_def fun_eq_iff Collect_def) + +lemma DEF_INSERT: + "insert = (%u ua y. y \ ua | y = u)" + unfolding mem_def fun_eq_iff insert_code by blast + +lemma DEF_IMAGE: + "op ` = (\u ua. {ub. \y. (\x. x \ ua \ y = u x) \ ub = y})" + by (simp add: fun_eq_iff image_def Bex_def) + +lemma DEF_GSPEC: + "Collect = (\u. u)" + by (simp add: Collect_def ext) + +lemma DEF_GEQ: + "(op =) = (op =)" + by simp + +lemma DEF_GABS: + "Eps = Eps" + by simp + +lemma DEF_FST: + "fst = (%p. SOME x. EX y. p = (x, y))" + unfolding fun_eq_iff + by (rule someI2) (auto intro: fst_conv[symmetric] someI2) + +lemma DEF_FINITE: + "finite = (\a. \FP. (\a. a = {} \ (\x s. a = insert x s \ FP s) \ FP a) \ FP a)" + unfolding fun_eq_iff + apply (intro allI iffI impI) + apply (erule finite_induct) + apply auto[2] + apply (drule_tac x="finite" in spec) + apply auto + apply (metis Collect_def Collect_empty_eq finite.emptyI) + by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1) + +lemma DEF_FACT: + "fact = (SOME FACT. FACT 0 = 1 & (\n. FACT (Suc n) = Suc n * FACT n))" + apply (rule some_equality[symmetric]) + apply (simp_all) + unfolding fun_eq_iff + apply (intro allI) + apply (induct_tac x) + apply simp_all done -lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))" - apply (rule ext, rule someI2) - apply (auto intro: snd_conv[symmetric]) +lemma DEF_EXP: + "power = (SOME EXP. (\m. EXP m 0 = 1) \ (\m n. EXP m (Suc n) = m * EXP m n))" + apply (rule some_equality[symmetric]) + apply (simp_all) + unfolding fun_eq_iff + apply (intro allI) + apply (induct_tac xa) + apply simp_all + done + +lemma DEF_EVEN: + "even = (SOME EVEN. EVEN 0 = True \ (\n. EVEN (Suc n) = (\ EVEN n)))" + apply (rule some_equality[symmetric]) + apply simp + unfolding fun_eq_iff + apply (intro allI) + apply (induct_tac x) + apply simp_all done -lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))" +lemma DEF_EMPTY: "{} = (%x. False)" + unfolding fun_eq_iff empty_def + by auto + +lemma DEF_DIV: + "op div = (SOME q. \r. \m n. if n = (0 :: nat) then q m n = 0 \ r m n = m + else m = q m n * n + r m n \ r m n < n)" + apply (rule some_equality[symmetric]) + apply (rule_tac x="op mod" in exI) + apply (auto simp add: fun_eq_iff) + apply (case_tac "xa = 0") + apply auto + apply (drule_tac x="x" in spec) + apply (drule_tac x="xa" in spec) + apply auto + by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less + nat_add_commute nat_mult_commute plus_nat.add_0) + +definition [hol4rew]: "DISJOINT a b \ a \ b = {}" + +lemma DEF_DISJOINT: + "DISJOINT = (%u ua. u \ ua = {})" + by (auto simp add: DISJOINT_def_raw) + +lemma DEF_DIFF: + "op - = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" + by (simp add: fun_eq_iff Collect_def) + (metis DiffE DiffI mem_def) + +definition [hol4rew]: "DELETE s e = s - {e}" + +lemma DEF_DELETE: + "DELETE = (\u ua. {ub. \y. (y \ u \ y \ ua) \ ub = y})" + by (auto simp add: DELETE_def_raw) + +lemma COND_DEF: + "(if b then t else f) = (SOME x. (b = True \ x = t) \ (b = False \ x = f))" + by auto + +definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)" + +lemma BIT1_DEF: + "NUMERAL_BIT1 = (%u. Suc (2 * u))" + by (auto) + +definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n" + +lemma BIT0_DEF: + "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \ (\n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))" + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext) + apply (induct_tac x) + apply auto + done + +lemma [hol4rew]: + "NUMERAL_BIT0 n = 2 * n" + "NUMERAL_BIT1 n = 2 * n + 1" + "2 * 0 = (0 :: nat)" + "2 * 1 = (2 :: nat)" + "0 + 1 = (1 :: nat)" + by simp_all + +lemma DEF_MINUS: "op - = (SOME sub. (\m. sub m 0 = m) & (\m n. sub m (Suc n) = sub m n - Suc 0))" + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext)+ + apply (induct_tac xa) + apply auto + done + +lemma DEF_PLUS: "op + = (SOME add. (\n. add 0 n = n) & (\m n. add (Suc m) n = Suc (add m n)))" apply (rule some_equality[symmetric]) apply auto apply (rule ext)+ @@ -65,39 +340,24 @@ apply auto done -lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))" - apply (rule some_equality[symmetric]) - apply auto - apply (rule ext)+ - apply (induct_tac x) - apply auto - done +lemmas [hol4rew] = id_apply -lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))" - apply (simp add: Pred_def) - apply (rule some_equality[symmetric]) - apply auto - apply (rule ext)+ - apply (induct_tac xa) - apply auto - done +lemma DEF_CHOICE: "Eps = (%u. SOME x. x \ u)" + by (simp add: mem_def) + +definition dotdot :: "nat => nat => nat => bool" + where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}" -definition NUMERAL_BIT0 :: "nat \ nat" where - "NUMERAL_BIT0 n \ n + n" - -lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)" - by (simp add: NUMERAL_BIT1_def) - -consts - sumlift :: "('a \ 'c) \ ('b \ 'c) \ (('a + 'b) \ 'c)" +lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})" + by (simp add: dotdot_def) -primrec - "sumlift f g (Inl a) = f a" - "sumlift f g (Inr b) = g b" - -lemma sum_Recursion: "\ f. (\ a. f (Inl a) = Inl' a) \ (\ b. f (Inr b) = Inr' b)" - apply (rule exI[where x="sumlift Inl' Inr'"]) - apply auto - done +lemma [hol4rew]: "dotdot a b = {a..b}" + unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def + by (simp add: Collect_conj_eq) + +definition [hol4rew,simp]: "INFINITE S \ \ finite S" + +lemma DEF_INFINITE: "INFINITE = (\u. \finite u)" + by (simp add: INFINITE_def_raw) end