--- a/src/HOL/Import/HOLLightCompat.thy Sat Mar 03 21:42:41 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,350 +0,0 @@
-(* Title: HOL/Import/HOLLightCompat.thy
- Author: Steven Obua and Sebastian Skalberg, TU Muenchen
- Author: Cezary Kaliszyk
-*)
-
-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:
- "\<forall>v. v = ()"
- by simp
-
-lemma num_Axiom:
- "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
- apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
- apply (auto simp add: fun_eq_iff)
- apply (induct_tac x)
- apply simp_all
- done
-
-lemma SUC_INJ:
- "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
- by simp
-
-lemma PAIR:
- "(fst x, snd x) = x"
- by simp
-
-lemma EXISTS_UNIQUE_THM:
- "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
- by auto
-
-lemma DEF__star_:
- "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
- apply (rule some_equality[symmetric])
- apply (auto simp add: fun_eq_iff)
- apply (induct_tac x)
- apply auto
- done
-
-lemma DEF__slash__backslash_:
- "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
- unfolding fun_eq_iff
- by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
-
-lemma DEF__lessthan__equal_:
- "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)))"
- 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. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> 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 \<ge>) = (%u ua. ua \<le> u)"
- by (simp)
-
-lemma DEF__greaterthan_:
- "(op >) = (%u ua. ua < u)"
- by (simp)
-
-lemma DEF__equal__equal__greaterthan_:
- "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
- by auto
-
-lemma DEF_WF:
- "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
- unfolding fun_eq_iff
-proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
- fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
- assume "P xa"
- then show "xa \<in> Collect P" by simp
-next
- fix x P xa z
- assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
- then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
-next
- fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
- assume a: "xa \<in> Q"
- assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
- then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
- then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
-qed
-
-lemma DEF_UNIV: "top = (%x. True)"
- by (rule ext) (simp add: top1I)
-
-lemma DEF_UNIONS:
- "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
- by (auto simp add: Union_eq)
-
-lemma DEF_UNION:
- "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
- by auto
-
-lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
- by (metis set_rev_mp subsetI)
-
-lemma DEF_SND:
- "snd = (\<lambda>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 \<longleftrightarrow> P & x = y"
-
-lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
- by (metis psubset_eq)
-
-definition [hol4rew]: "Pred n = n - (Suc 0)"
-
-lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
- apply (rule some_equality[symmetric])
- apply (simp add: Pred_def)
- apply (rule ext)
- apply (induct_tac x)
- apply (auto simp add: Pred_def)
- done
-
-lemma DEF_ONE_ONE:
- "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
- by (simp add: inj_on_def)
-
-definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
-
-lemma DEF_ODD:
- "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
- apply (rule some_equality[symmetric])
- apply simp
- unfolding fun_eq_iff
- apply (intro allI)
- apply (induct_tac x)
- apply simp_all
- done
-
-definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
-
-lemma DEF_MOD:
- "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
- r m n = m else m = m div n * n + r m n \<and> 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. (a, b) \<in> measure u)"
- unfolding MEASURE_def measure_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 = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
- by auto
-
-lemma DEF_INTER:
- "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
- by auto
-
-lemma DEF_INSERT:
- "insert = (\<lambda>u ua. {y. y \<in> ua | y = u})"
- by auto
-
-lemma DEF_IMAGE:
- "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
- by (simp add: fun_eq_iff image_def Bex_def)
-
-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 = (\<lambda>a. \<forall>FP. (\<forall>a. a = {} \<or> (\<exists>x s. a = insert x s \<and> FP s) \<longrightarrow> FP a) \<longrightarrow> 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)
- by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
-
-lemma DEF_FACT:
- "fact = (SOME FACT. FACT 0 = 1 & (\<forall>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 DEF_EXP:
- "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>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 \<and> (\<forall>n. EVEN (Suc n) = (\<not> 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 DEF_EMPTY: "bot = (%x. False)"
- by (rule ext) auto
-
-lemma DEF_DIV:
- "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
- else m = q m n * n + r m n \<and> 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 \<longleftrightarrow> a \<inter> b = {}"
-
-lemma DEF_DISJOINT:
- "DISJOINT = (%u ua. u \<inter> ua = {})"
- by (auto simp add: DISJOINT_def_raw)
-
-lemma DEF_DIFF:
- "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
- by (metis set_diff_eq)
-
-definition [hol4rew]: "DELETE s e = s - {e}"
-
-lemma DEF_DELETE:
- "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
- by (auto simp add: DELETE_def_raw)
-
-lemma COND_DEF:
- "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> 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 \<and> (\<forall>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. (\<forall>m. sub m 0 = m) & (\<forall>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. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
- apply (rule some_equality[symmetric])
- apply auto
- apply (rule ext)+
- apply (induct_tac x)
- apply auto
- done
-
-lemmas [hol4rew] = id_apply
-
-lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)"
- by simp
-
-definition dotdot :: "nat => nat => nat set"
- where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
-
-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 \<longleftrightarrow> \<not> finite S"
-
-lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
- by (simp add: INFINITE_def_raw)
-
-end
-