1.1 --- a/src/HOL/Import/HOLLightCompat.thy Wed Jul 13 00:29:33 2011 +0900
1.2 +++ b/src/HOL/Import/HOLLightCompat.thy Wed Jul 13 00:43:07 2011 +0900
1.3 @@ -1,38 +1,139 @@
1.4 (* Title: HOL/Import/HOLLightCompat.thy
1.5 Author: Steven Obua and Sebastian Skalberg, TU Muenchen
1.6 + Author: Cezary Kaliszyk
1.7 *)
1.8
1.9 -theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
1.10 +theory HOLLightCompat
1.11 +imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
1.12 + HOLLightList HOLLightReal HOLLightInt HOL4Setup
1.13 +begin
1.14
1.15 -lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
1.16 - by auto;
1.17 +(* list *)
1.18 +lemmas [hol4rew] = list_el_def member_def list_mem_def
1.19 +(* int *)
1.20 +lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def
1.21 +(* real *)
1.22 +lemma [hol4rew]:
1.23 + "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2"
1.24 + by simp_all
1.25
1.26 -lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
1.27 +lemma one:
1.28 + "\<forall>v. v = ()"
1.29 by simp
1.30
1.31 -lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
1.32 -proof auto
1.33 - assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
1.34 - have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
1.35 - with a
1.36 - have "t1 = True"
1.37 - by (rule comb_rule)
1.38 - thus t1
1.39 - by simp
1.40 -next
1.41 - assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
1.42 - have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
1.43 - with a
1.44 - have "t2 = True"
1.45 - by (rule comb_rule)
1.46 - thus t2
1.47 - by simp
1.48 -qed
1.49 +lemma num_Axiom:
1.50 + "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
1.51 + apply (intro allI)
1.52 + apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
1.53 + apply auto
1.54 + apply (simp add: fun_eq_iff)
1.55 + apply (intro allI)
1.56 + apply (induct_tac xa)
1.57 + apply simp_all
1.58 + done
1.59
1.60 -definition Pred :: "nat \<Rightarrow> nat" where
1.61 - "Pred n \<equiv> n - (Suc 0)"
1.62 +lemma SUC_INJ:
1.63 + "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
1.64 + by auto
1.65
1.66 -lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
1.67 +lemma PAIR:
1.68 + "(fst x, snd x) = x"
1.69 + by simp
1.70 +
1.71 +lemma EXISTS_UNIQUE_THM:
1.72 + "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
1.73 + by auto
1.74 +
1.75 +lemma DEF__star_:
1.76 + "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
1.77 + apply (rule some_equality[symmetric])
1.78 + apply auto
1.79 + apply (rule ext)+
1.80 + apply (induct_tac x)
1.81 + apply auto
1.82 + done
1.83 +
1.84 +lemma DEF__slash__backslash_:
1.85 + "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
1.86 + unfolding fun_eq_iff
1.87 + by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
1.88 +
1.89 +lemma DEF__lessthan__equal_:
1.90 + "op \<le> = (SOME u. (\<forall>m. u m 0 = (m = 0)) \<and> (\<forall>m n. u m (Suc n) = (m = Suc n \<or> u m n)))"
1.91 + apply (rule some_equality[symmetric])
1.92 + apply auto[1]
1.93 + apply (simp add: fun_eq_iff)
1.94 + apply (intro allI)
1.95 + apply (induct_tac xa)
1.96 + apply auto
1.97 + done
1.98 +
1.99 +lemma DEF__lessthan_:
1.100 + "op < = (SOME u. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> u m n)))"
1.101 + apply (rule some_equality[symmetric])
1.102 + apply auto[1]
1.103 + apply (simp add: fun_eq_iff)
1.104 + apply (intro allI)
1.105 + apply (induct_tac xa)
1.106 + apply auto
1.107 + done
1.108 +
1.109 +lemma DEF__greaterthan__equal_:
1.110 + "(op \<ge>) = (%u ua. ua \<le> u)"
1.111 + by (simp)
1.112 +
1.113 +lemma DEF__greaterthan_:
1.114 + "(op >) = (%u ua. ua < u)"
1.115 + by (simp)
1.116 +
1.117 +lemma DEF__equal__equal__greaterthan_:
1.118 + "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
1.119 + by auto
1.120 +
1.121 +lemma DEF_WF:
1.122 + "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
1.123 + unfolding fun_eq_iff
1.124 + apply (intro allI, rule, intro allI impI, elim exE)
1.125 + apply (drule_tac wfE_min[to_pred, unfolded mem_def])
1.126 + apply assumption
1.127 + prefer 2
1.128 + apply assumption
1.129 + apply auto[1]
1.130 + apply (intro wfI_min[to_pred, unfolded mem_def])
1.131 + apply (drule_tac x="Q" in spec)
1.132 + apply auto
1.133 + apply (rule_tac x="xb" in bexI)
1.134 + apply (auto simp add: mem_def)
1.135 + done
1.136 +
1.137 +lemma DEF_UNIV: "UNIV = (%x. True)"
1.138 + by (auto simp add: mem_def)
1.139 +
1.140 +lemma DEF_UNIONS:
1.141 + "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
1.142 + by (simp add: fun_eq_iff Collect_def)
1.143 + (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
1.144 +
1.145 +lemma DEF_UNION:
1.146 + "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
1.147 + by (auto simp add: mem_def fun_eq_iff Collect_def)
1.148 +
1.149 +lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
1.150 + by (metis set_rev_mp subsetI)
1.151 +
1.152 +lemma DEF_SND:
1.153 + "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
1.154 + unfolding fun_eq_iff
1.155 + by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
1.156 +
1.157 +definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
1.158 +
1.159 +lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
1.160 + by (auto simp add: mem_def fun_eq_iff)
1.161 +
1.162 +definition [hol4rew]: "Pred n = n - (Suc 0)"
1.163 +
1.164 +lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
1.165 apply (rule some_equality[symmetric])
1.166 apply (simp add: Pred_def)
1.167 apply (rule ext)
1.168 @@ -40,24 +141,198 @@
1.169 apply (auto simp add: Pred_def)
1.170 done
1.171
1.172 -lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
1.173 +lemma DEF_ONE_ONE:
1.174 + "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
1.175 + by (simp add: inj_on_def)
1.176
1.177 -lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
1.178 - apply (subst Abs_Prod_inverse)
1.179 - apply (auto simp add: Prod_def)
1.180 +definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
1.181 +
1.182 +lemma DEF_ODD:
1.183 + "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
1.184 + apply (rule some_equality[symmetric])
1.185 + apply simp
1.186 + unfolding fun_eq_iff
1.187 + apply (intro allI)
1.188 + apply (induct_tac x)
1.189 + apply simp_all
1.190 done
1.191
1.192 -lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
1.193 - apply (rule ext, rule someI2)
1.194 - apply (auto intro: fst_conv[symmetric])
1.195 +definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
1.196 +
1.197 +lemma DEF_MOD:
1.198 + "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
1.199 + r m n = m else m = m div n * n + r m n \<and> r m n < n)"
1.200 + apply (rule some_equality[symmetric])
1.201 + apply (auto simp add: fun_eq_iff)
1.202 + apply (case_tac "xa = 0")
1.203 + apply auto
1.204 + apply (drule_tac x="x" in spec)
1.205 + apply (drule_tac x="xa" in spec)
1.206 + apply auto
1.207 + by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
1.208 +
1.209 +definition "MEASURE = (%u x y. (u x :: nat) < u y)"
1.210 +
1.211 +lemma [hol4rew]:
1.212 + "MEASURE u = (%a b. measure u (a, b))"
1.213 + unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
1.214 + by simp
1.215 +
1.216 +definition
1.217 + "LET f s = f s"
1.218 +
1.219 +lemma [hol4rew]:
1.220 + "LET f s = Let s f"
1.221 + by (simp add: LET_def Let_def)
1.222 +
1.223 +lemma DEF_INTERS:
1.224 + "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
1.225 + by (auto simp add: fun_eq_iff mem_def Collect_def)
1.226 + (metis InterD InterI mem_def)+
1.227 +
1.228 +lemma DEF_INTER:
1.229 + "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
1.230 + by (auto simp add: mem_def fun_eq_iff Collect_def)
1.231 +
1.232 +lemma DEF_INSERT:
1.233 + "insert = (%u ua y. y \<in> ua | y = u)"
1.234 + unfolding mem_def fun_eq_iff insert_code by blast
1.235 +
1.236 +lemma DEF_IMAGE:
1.237 + "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
1.238 + by (simp add: fun_eq_iff image_def Bex_def)
1.239 +
1.240 +lemma DEF_GSPEC:
1.241 + "Collect = (\<lambda>u. u)"
1.242 + by (simp add: Collect_def ext)
1.243 +
1.244 +lemma DEF_GEQ:
1.245 + "(op =) = (op =)"
1.246 + by simp
1.247 +
1.248 +lemma DEF_GABS:
1.249 + "Eps = Eps"
1.250 + by simp
1.251 +
1.252 +lemma DEF_FST:
1.253 + "fst = (%p. SOME x. EX y. p = (x, y))"
1.254 + unfolding fun_eq_iff
1.255 + by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
1.256 +
1.257 +lemma DEF_FINITE:
1.258 + "finite = (\<lambda>a. \<forall>FP. (\<forall>a. a = {} \<or> (\<exists>x s. a = insert x s \<and> FP s) \<longrightarrow> FP a) \<longrightarrow> FP a)"
1.259 + unfolding fun_eq_iff
1.260 + apply (intro allI iffI impI)
1.261 + apply (erule finite_induct)
1.262 + apply auto[2]
1.263 + apply (drule_tac x="finite" in spec)
1.264 + apply auto
1.265 + apply (metis Collect_def Collect_empty_eq finite.emptyI)
1.266 + by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
1.267 +
1.268 +lemma DEF_FACT:
1.269 + "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
1.270 + apply (rule some_equality[symmetric])
1.271 + apply (simp_all)
1.272 + unfolding fun_eq_iff
1.273 + apply (intro allI)
1.274 + apply (induct_tac x)
1.275 + apply simp_all
1.276 done
1.277
1.278 -lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
1.279 - apply (rule ext, rule someI2)
1.280 - apply (auto intro: snd_conv[symmetric])
1.281 +lemma DEF_EXP:
1.282 + "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
1.283 + apply (rule some_equality[symmetric])
1.284 + apply (simp_all)
1.285 + unfolding fun_eq_iff
1.286 + apply (intro allI)
1.287 + apply (induct_tac xa)
1.288 + apply simp_all
1.289 done
1.290
1.291 -lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
1.292 +lemma DEF_EVEN:
1.293 + "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
1.294 + apply (rule some_equality[symmetric])
1.295 + apply simp
1.296 + unfolding fun_eq_iff
1.297 + apply (intro allI)
1.298 + apply (induct_tac x)
1.299 + apply simp_all
1.300 + done
1.301 +
1.302 +lemma DEF_EMPTY: "{} = (%x. False)"
1.303 + unfolding fun_eq_iff empty_def
1.304 + by auto
1.305 +
1.306 +lemma DEF_DIV:
1.307 + "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
1.308 + else m = q m n * n + r m n \<and> r m n < n)"
1.309 + apply (rule some_equality[symmetric])
1.310 + apply (rule_tac x="op mod" in exI)
1.311 + apply (auto simp add: fun_eq_iff)
1.312 + apply (case_tac "xa = 0")
1.313 + apply auto
1.314 + apply (drule_tac x="x" in spec)
1.315 + apply (drule_tac x="xa" in spec)
1.316 + apply auto
1.317 + by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
1.318 + nat_add_commute nat_mult_commute plus_nat.add_0)
1.319 +
1.320 +definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
1.321 +
1.322 +lemma DEF_DISJOINT:
1.323 + "DISJOINT = (%u ua. u \<inter> ua = {})"
1.324 + by (auto simp add: DISJOINT_def_raw)
1.325 +
1.326 +lemma DEF_DIFF:
1.327 + "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
1.328 + by (simp add: fun_eq_iff Collect_def)
1.329 + (metis DiffE DiffI mem_def)
1.330 +
1.331 +definition [hol4rew]: "DELETE s e = s - {e}"
1.332 +
1.333 +lemma DEF_DELETE:
1.334 + "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
1.335 + by (auto simp add: DELETE_def_raw)
1.336 +
1.337 +lemma COND_DEF:
1.338 + "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
1.339 + by auto
1.340 +
1.341 +definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
1.342 +
1.343 +lemma BIT1_DEF:
1.344 + "NUMERAL_BIT1 = (%u. Suc (2 * u))"
1.345 + by (auto)
1.346 +
1.347 +definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
1.348 +
1.349 +lemma BIT0_DEF:
1.350 + "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
1.351 + apply (rule some_equality[symmetric])
1.352 + apply auto
1.353 + apply (rule ext)
1.354 + apply (induct_tac x)
1.355 + apply auto
1.356 + done
1.357 +
1.358 +lemma [hol4rew]:
1.359 + "NUMERAL_BIT0 n = 2 * n"
1.360 + "NUMERAL_BIT1 n = 2 * n + 1"
1.361 + "2 * 0 = (0 :: nat)"
1.362 + "2 * 1 = (2 :: nat)"
1.363 + "0 + 1 = (1 :: nat)"
1.364 + by simp_all
1.365 +
1.366 +lemma DEF_MINUS: "op - = (SOME sub. (\<forall>m. sub m 0 = m) & (\<forall>m n. sub m (Suc n) = sub m n - Suc 0))"
1.367 + apply (rule some_equality[symmetric])
1.368 + apply auto
1.369 + apply (rule ext)+
1.370 + apply (induct_tac xa)
1.371 + apply auto
1.372 + done
1.373 +
1.374 +lemma DEF_PLUS: "op + = (SOME add. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
1.375 apply (rule some_equality[symmetric])
1.376 apply auto
1.377 apply (rule ext)+
1.378 @@ -65,39 +340,24 @@
1.379 apply auto
1.380 done
1.381
1.382 -lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
1.383 - apply (rule some_equality[symmetric])
1.384 - apply auto
1.385 - apply (rule ext)+
1.386 - apply (induct_tac x)
1.387 - apply auto
1.388 - done
1.389 +lemmas [hol4rew] = id_apply
1.390
1.391 -lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
1.392 - apply (simp add: Pred_def)
1.393 - apply (rule some_equality[symmetric])
1.394 - apply auto
1.395 - apply (rule ext)+
1.396 - apply (induct_tac xa)
1.397 - apply auto
1.398 - done
1.399 +lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
1.400 + by (simp add: mem_def)
1.401
1.402 -definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where
1.403 - "NUMERAL_BIT0 n \<equiv> n + n"
1.404 +definition dotdot :: "nat => nat => nat => bool"
1.405 + where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
1.406
1.407 -lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
1.408 - by (simp add: NUMERAL_BIT1_def)
1.409 +lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
1.410 + by (simp add: dotdot_def)
1.411
1.412 -consts
1.413 - sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
1.414 +lemma [hol4rew]: "dotdot a b = {a..b}"
1.415 + unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
1.416 + by (simp add: Collect_conj_eq)
1.417
1.418 -primrec
1.419 - "sumlift f g (Inl a) = f a"
1.420 - "sumlift f g (Inr b) = g b"
1.421 -
1.422 -lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
1.423 - apply (rule exI[where x="sumlift Inl' Inr'"])
1.424 - apply auto
1.425 - done
1.426 +definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
1.427 +
1.428 +lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
1.429 + by (simp add: INFINITE_def_raw)
1.430
1.431 end