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