src/HOL/Import/HOLLightCompat.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jul 13 00:43:07 2011 +0900 (2011-07-13)
changeset 43787 5be84619e4d4
parent 41589 bbd861837ebc
child 44633 8a2fd7418435
permissions -rw-r--r--
Update HOLLightCompat
     1 (*  Title:      HOL/Import/HOLLightCompat.thy
     2     Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
     3     Author:     Cezary Kaliszyk
     4 *)
     5 
     6 theory HOLLightCompat
     7 imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
     8   HOLLightList HOLLightReal HOLLightInt HOL4Setup
     9 begin
    10 
    11 (* list *)
    12 lemmas [hol4rew] = list_el_def member_def list_mem_def
    13 (* int *)
    14 lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def
    15 (* real *)
    16 lemma [hol4rew]:
    17   "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2"
    18   by simp_all
    19 
    20 lemma one:
    21   "\<forall>v. v = ()"
    22   by simp
    23 
    24 lemma num_Axiom:
    25   "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
    26   apply (intro allI)
    27   apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
    28   apply auto
    29   apply (simp add: fun_eq_iff)
    30   apply (intro allI)
    31   apply (induct_tac xa)
    32   apply simp_all
    33   done
    34 
    35 lemma SUC_INJ:
    36   "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
    37   by auto
    38 
    39 lemma PAIR:
    40   "(fst x, snd x) = x"
    41   by simp
    42 
    43 lemma EXISTS_UNIQUE_THM:
    44   "(Ex1 P) = (Ex P & (\<forall>x y. P x & P y --> (x = y)))"
    45   by auto
    46 
    47 lemma DEF__star_:
    48   "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
    49   apply (rule some_equality[symmetric])
    50   apply auto
    51   apply (rule ext)+
    52   apply (induct_tac x)
    53   apply auto
    54   done
    55 
    56 lemma DEF__slash__backslash_:
    57   "(t1 \<and> t2) = ((\<lambda>f. f t1 t2 :: bool) = (\<lambda>f. f True True))"
    58   unfolding fun_eq_iff
    59   by (intro iffI, simp_all) (erule allE[of _ "(%a b. a \<and> b)"], simp)
    60 
    61 lemma DEF__lessthan__equal_:
    62   "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)))"
    63   apply (rule some_equality[symmetric])
    64   apply auto[1]
    65   apply (simp add: fun_eq_iff)
    66   apply (intro allI)
    67   apply (induct_tac xa)
    68   apply auto
    69   done
    70 
    71 lemma DEF__lessthan_:
    72   "op < = (SOME u. (\<forall>m. u m 0 = False) \<and> (\<forall>m n. u m (Suc n) = (m = n \<or> u m n)))"
    73   apply (rule some_equality[symmetric])
    74   apply auto[1]
    75   apply (simp add: fun_eq_iff)
    76   apply (intro allI)
    77   apply (induct_tac xa)
    78   apply auto
    79   done
    80 
    81 lemma DEF__greaterthan__equal_:
    82   "(op \<ge>) = (%u ua. ua \<le> u)"
    83   by (simp)
    84 
    85 lemma DEF__greaterthan_:
    86   "(op >) = (%u ua. ua < u)"
    87   by (simp)
    88 
    89 lemma DEF__equal__equal__greaterthan_:
    90   "(t1 \<longrightarrow> t2) = ((t1 \<and> t2) = t1)"
    91   by auto
    92 
    93 lemma DEF_WF:
    94   "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
    95   unfolding fun_eq_iff
    96   apply (intro allI, rule, intro allI impI, elim exE)
    97   apply (drule_tac wfE_min[to_pred, unfolded mem_def])
    98   apply assumption
    99   prefer 2
   100   apply assumption
   101   apply auto[1]
   102   apply (intro wfI_min[to_pred, unfolded mem_def])
   103   apply (drule_tac x="Q" in spec)
   104   apply auto
   105   apply (rule_tac x="xb" in bexI)
   106   apply (auto simp add: mem_def)
   107   done
   108 
   109 lemma DEF_UNIV: "UNIV = (%x. True)"
   110   by (auto simp add: mem_def)
   111 
   112 lemma DEF_UNIONS:
   113   "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
   114   by (simp add: fun_eq_iff Collect_def)
   115      (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
   116 
   117 lemma DEF_UNION:
   118   "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
   119   by (auto simp add: mem_def fun_eq_iff Collect_def)
   120 
   121 lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
   122   by (metis set_rev_mp subsetI)
   123 
   124 lemma DEF_SND:
   125   "snd = (\<lambda>p. SOME x. EX y. p = (y, x))"
   126   unfolding fun_eq_iff
   127   by (rule someI2) (auto intro: snd_conv[symmetric] someI2)
   128 
   129 definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
   130 
   131 lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
   132   by (auto simp add: mem_def fun_eq_iff)
   133 
   134 definition [hol4rew]: "Pred n = n - (Suc 0)"
   135 
   136 lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\<forall>n. PRE (Suc n) = n))"
   137   apply (rule some_equality[symmetric])
   138   apply (simp add: Pred_def)
   139   apply (rule ext)
   140   apply (induct_tac x)
   141   apply (auto simp add: Pred_def)
   142   done
   143 
   144 lemma DEF_ONE_ONE:
   145   "inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
   146   by (simp add: inj_on_def)
   147 
   148 definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
   149 
   150 lemma DEF_ODD:
   151   "odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> ODD n)))"
   152   apply (rule some_equality[symmetric])
   153   apply simp
   154   unfolding fun_eq_iff
   155   apply (intro allI)
   156   apply (induct_tac x)
   157   apply simp_all
   158   done
   159 
   160 definition [hol4rew, simp]: "NUMERAL (x :: nat) = x"
   161 
   162 lemma DEF_MOD:
   163   "op mod = (SOME r. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
   164      r m n = m else m = m div n * n + r m n \<and> r m n < n)"
   165   apply (rule some_equality[symmetric])
   166   apply (auto simp add: fun_eq_iff)
   167   apply (case_tac "xa = 0")
   168   apply auto
   169   apply (drule_tac x="x" in spec)
   170   apply (drule_tac x="xa" in spec)
   171   apply auto
   172   by (metis mod_less mod_mult_self2 nat_add_commute nat_mult_commute)
   173 
   174 definition "MEASURE = (%u x y. (u x :: nat) < u y)"
   175 
   176 lemma [hol4rew]:
   177   "MEASURE u = (%a b. measure u (a, b))"
   178   unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
   179   by simp
   180 
   181 definition
   182   "LET f s = f s"
   183 
   184 lemma [hol4rew]:
   185   "LET f s = Let s f"
   186   by (simp add: LET_def Let_def)
   187 
   188 lemma DEF_INTERS:
   189   "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
   190   by (auto simp add: fun_eq_iff mem_def Collect_def)
   191      (metis InterD InterI mem_def)+
   192 
   193 lemma DEF_INTER:
   194   "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
   195   by (auto simp add: mem_def fun_eq_iff Collect_def)
   196 
   197 lemma DEF_INSERT:
   198   "insert = (%u ua y. y \<in> ua | y = u)"
   199   unfolding mem_def fun_eq_iff insert_code by blast
   200 
   201 lemma DEF_IMAGE:
   202   "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
   203   by (simp add: fun_eq_iff image_def Bex_def)
   204 
   205 lemma DEF_GSPEC:
   206   "Collect = (\<lambda>u. u)"
   207   by (simp add: Collect_def ext)
   208 
   209 lemma DEF_GEQ:
   210   "(op =) = (op =)"
   211   by simp
   212 
   213 lemma DEF_GABS:
   214   "Eps = Eps"
   215   by simp
   216 
   217 lemma DEF_FST:
   218   "fst = (%p. SOME x. EX y. p = (x, y))"
   219   unfolding fun_eq_iff
   220   by (rule someI2) (auto intro: fst_conv[symmetric] someI2)
   221 
   222 lemma DEF_FINITE:
   223   "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)"
   224   unfolding fun_eq_iff
   225   apply (intro allI iffI impI)
   226   apply (erule finite_induct)
   227   apply auto[2]
   228   apply (drule_tac x="finite" in spec)
   229   apply auto
   230   apply (metis Collect_def Collect_empty_eq finite.emptyI)
   231   by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
   232 
   233 lemma DEF_FACT:
   234   "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
   235   apply (rule some_equality[symmetric])
   236   apply (simp_all)
   237   unfolding fun_eq_iff
   238   apply (intro allI)
   239   apply (induct_tac x)
   240   apply simp_all
   241   done
   242 
   243 lemma DEF_EXP:
   244   "power = (SOME EXP. (\<forall>m. EXP m 0 = 1) \<and> (\<forall>m n. EXP m (Suc n) = m * EXP m n))"
   245   apply (rule some_equality[symmetric])
   246   apply (simp_all)
   247   unfolding fun_eq_iff
   248   apply (intro allI)
   249   apply (induct_tac xa)
   250   apply simp_all
   251   done
   252 
   253 lemma DEF_EVEN:
   254   "even = (SOME EVEN. EVEN 0 = True \<and> (\<forall>n. EVEN (Suc n) = (\<not> EVEN n)))"
   255   apply (rule some_equality[symmetric])
   256   apply simp
   257   unfolding fun_eq_iff
   258   apply (intro allI)
   259   apply (induct_tac x)
   260   apply simp_all
   261   done
   262 
   263 lemma DEF_EMPTY: "{} = (%x. False)"
   264   unfolding fun_eq_iff empty_def
   265   by auto
   266 
   267 lemma DEF_DIV:
   268   "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
   269      else m = q m n * n + r m n \<and> r m n < n)"
   270   apply (rule some_equality[symmetric])
   271   apply (rule_tac x="op mod" in exI)
   272   apply (auto simp add: fun_eq_iff)
   273   apply (case_tac "xa = 0")
   274   apply auto
   275   apply (drule_tac x="x" in spec)
   276   apply (drule_tac x="xa" in spec)
   277   apply auto
   278   by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less
   279       nat_add_commute nat_mult_commute plus_nat.add_0)
   280 
   281 definition [hol4rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
   282 
   283 lemma DEF_DISJOINT:
   284   "DISJOINT = (%u ua. u \<inter> ua = {})"
   285   by (auto simp add: DISJOINT_def_raw)
   286 
   287 lemma DEF_DIFF:
   288   "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
   289   by (simp add: fun_eq_iff Collect_def)
   290      (metis DiffE DiffI mem_def)
   291 
   292 definition [hol4rew]: "DELETE s e = s - {e}"
   293 
   294 lemma DEF_DELETE:
   295   "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
   296   by (auto simp add: DELETE_def_raw)
   297 
   298 lemma COND_DEF:
   299   "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
   300   by auto
   301 
   302 definition [simp]: "NUMERAL_BIT1 n = n + (n + Suc 0)"
   303 
   304 lemma BIT1_DEF:
   305   "NUMERAL_BIT1 = (%u. Suc (2 * u))"
   306   by (auto)
   307 
   308 definition [simp]: "NUMERAL_BIT0 (n :: nat) = n + n"
   309 
   310 lemma BIT0_DEF:
   311   "NUMERAL_BIT0 = (SOME BIT0. BIT0 0 = 0 \<and> (\<forall>n. BIT0 (Suc n) = Suc (Suc (BIT0 n))))"
   312   apply (rule some_equality[symmetric])
   313   apply auto
   314   apply (rule ext)
   315   apply (induct_tac x)
   316   apply auto
   317   done
   318 
   319 lemma [hol4rew]:
   320   "NUMERAL_BIT0 n = 2 * n"
   321   "NUMERAL_BIT1 n = 2 * n + 1"
   322   "2 * 0 = (0 :: nat)"
   323   "2 * 1 = (2 :: nat)"
   324   "0 + 1 = (1 :: nat)"
   325   by simp_all
   326 
   327 lemma DEF_MINUS: "op - = (SOME sub. (\<forall>m. sub m 0 = m) & (\<forall>m n. sub m (Suc n) = sub m n - Suc 0))"
   328   apply (rule some_equality[symmetric])
   329   apply auto
   330   apply (rule ext)+
   331   apply (induct_tac xa)
   332   apply auto
   333   done
   334 
   335 lemma DEF_PLUS: "op + = (SOME add. (\<forall>n. add 0 n = n) & (\<forall>m n. add (Suc m) n = Suc (add m n)))"
   336   apply (rule some_equality[symmetric])
   337   apply auto
   338   apply (rule ext)+
   339   apply (induct_tac x)
   340   apply auto
   341   done
   342 
   343 lemmas [hol4rew] = id_apply
   344 
   345 lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
   346   by (simp add: mem_def)
   347 
   348 definition dotdot :: "nat => nat => nat => bool"
   349   where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
   350 
   351 lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
   352   by (simp add: dotdot_def)
   353 
   354 lemma [hol4rew]: "dotdot a b = {a..b}"
   355   unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
   356   by (simp add: Collect_conj_eq)
   357 
   358 definition [hol4rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
   359 
   360 lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
   361   by (simp add: INFINITE_def_raw)
   362 
   363 end