# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# 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:
+  "\<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