--- 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:
+ "\<forall>v. v = ()"
+ by simp
-lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
- by auto;
+lemma num_Axiom:
+ "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>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:
+ "\<forall>m n. Suc m = Suc n \<longleftrightarrow> 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 & (\<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
+ apply (rule ext)+
+ 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)
-definition Pred :: "nat \<Rightarrow> nat" where
- "Pred n \<equiv> n - (Suc 0)"
+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
+ 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 = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
+ by (simp add: fun_eq_iff Collect_def)
+ (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
+
+lemma DEF_UNION:
+ "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
+ by (auto simp add: mem_def fun_eq_iff Collect_def)
+
+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 (auto simp add: mem_def fun_eq_iff)
+
+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)
@@ -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 = (\<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 REP_ABS_PAIR: "\<forall> 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 \<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
-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. \<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. 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 = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
+ by (auto simp add: fun_eq_iff mem_def Collect_def)
+ (metis InterD InterI mem_def)+
+
+lemma DEF_INTER:
+ "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
+ by (auto simp add: mem_def fun_eq_iff Collect_def)
+
+lemma DEF_INSERT:
+ "insert = (%u ua y. y \<in> ua | y = u)"
+ unfolding mem_def fun_eq_iff insert_code by blast
+
+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_GSPEC:
+ "Collect = (\<lambda>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 = (\<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)
+ 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 & (\<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 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. (\<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 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. \<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 (simp add: fun_eq_iff Collect_def)
+ (metis DiffE DiffI mem_def)
+
+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)+
@@ -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 \<in> 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 \<Rightarrow> nat" where
- "NUMERAL_BIT0 n \<equiv> n + n"
-
-lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
- by (simp add: NUMERAL_BIT1_def)
-
-consts
- sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> '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: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> 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 \<longleftrightarrow> \<not> finite S"
+
+lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
+ by (simp add: INFINITE_def_raw)
end