src/HOL/Import/HOLLightCompat.thy

HOL/Import: observe distinction between sets and predicates (where possible)

(*  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 = (%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_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. x \<in> u)"
  by (simp add: mem_def)

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