src/HOL/Import/HOLLightCompat.thy
changeset 44633 8a2fd7418435
parent 43787 5be84619e4d4
child 46782 d50855d9ea74
     1.1 --- a/src/HOL/Import/HOLLightCompat.thy	Wed Aug 31 13:28:29 2011 -0700
     1.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Thu Sep 01 16:16:25 2011 +0900
     1.3 @@ -22,19 +22,16 @@
     1.4    by simp
     1.5  
     1.6  lemma num_Axiom:
     1.7 -  "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
     1.8 -  apply (intro allI)
     1.9 -  apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
    1.10 -  apply auto
    1.11 -  apply (simp add: fun_eq_iff)
    1.12 -  apply (intro allI)
    1.13 -  apply (induct_tac xa)
    1.14 +  "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
    1.15 +  apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
    1.16 +  apply (auto simp add: fun_eq_iff)
    1.17 +  apply (induct_tac x)
    1.18    apply simp_all
    1.19    done
    1.20  
    1.21  lemma SUC_INJ:
    1.22    "\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
    1.23 -  by auto
    1.24 +  by simp
    1.25  
    1.26  lemma PAIR:
    1.27    "(fst x, snd x) = x"
    1.28 @@ -47,8 +44,7 @@
    1.29  lemma DEF__star_:
    1.30    "op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
    1.31    apply (rule some_equality[symmetric])
    1.32 -  apply auto
    1.33 -  apply (rule ext)+
    1.34 +  apply (auto simp add: fun_eq_iff)
    1.35    apply (induct_tac x)
    1.36    apply auto
    1.37    done
    1.38 @@ -93,30 +89,32 @@
    1.39  lemma DEF_WF:
    1.40    "wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
    1.41    unfolding fun_eq_iff
    1.42 -  apply (intro allI, rule, intro allI impI, elim exE)
    1.43 -  apply (drule_tac wfE_min[to_pred, unfolded mem_def])
    1.44 -  apply assumption
    1.45 -  prefer 2
    1.46 -  apply assumption
    1.47 -  apply auto[1]
    1.48 -  apply (intro wfI_min[to_pred, unfolded mem_def])
    1.49 -  apply (drule_tac x="Q" in spec)
    1.50 -  apply auto
    1.51 -  apply (rule_tac x="xb" in bexI)
    1.52 -  apply (auto simp add: mem_def)
    1.53 -  done
    1.54 +proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
    1.55 +  fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
    1.56 +  assume "P xa"
    1.57 +  then show "xa \<in> Collect P" by simp
    1.58 +next
    1.59 +  fix x P xa z
    1.60 +  assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
    1.61 +  then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
    1.62 +next
    1.63 +  fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
    1.64 +  assume a: "xa \<in> Q"
    1.65 +  assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
    1.66 +  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
    1.67 +  then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
    1.68 +qed
    1.69  
    1.70 -lemma DEF_UNIV: "UNIV = (%x. True)"
    1.71 -  by (auto simp add: mem_def)
    1.72 +lemma DEF_UNIV: "top = (%x. True)"
    1.73 +  by (rule ext) (simp add: top1I)
    1.74  
    1.75  lemma DEF_UNIONS:
    1.76    "Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
    1.77 -  by (simp add: fun_eq_iff Collect_def)
    1.78 -     (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
    1.79 +  by (auto simp add: Union_eq)
    1.80  
    1.81  lemma DEF_UNION:
    1.82    "op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
    1.83 -  by (auto simp add: mem_def fun_eq_iff Collect_def)
    1.84 +  by auto
    1.85  
    1.86  lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
    1.87    by (metis set_rev_mp subsetI)
    1.88 @@ -129,7 +127,7 @@
    1.89  definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
    1.90  
    1.91  lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
    1.92 -  by (auto simp add: mem_def fun_eq_iff)
    1.93 +  by (metis psubset_eq)
    1.94  
    1.95  definition [hol4rew]: "Pred n = n - (Suc 0)"
    1.96  
    1.97 @@ -174,8 +172,8 @@
    1.98  definition "MEASURE = (%u x y. (u x :: nat) < u y)"
    1.99  
   1.100  lemma [hol4rew]:
   1.101 -  "MEASURE u = (%a b. measure u (a, b))"
   1.102 -  unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
   1.103 +  "MEASURE u = (%a b. (a, b) \<in> measure u)"
   1.104 +  unfolding MEASURE_def measure_def
   1.105    by simp
   1.106  
   1.107  definition
   1.108 @@ -187,12 +185,11 @@
   1.109  
   1.110  lemma DEF_INTERS:
   1.111    "Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
   1.112 -  by (auto simp add: fun_eq_iff mem_def Collect_def)
   1.113 -     (metis InterD InterI mem_def)+
   1.114 +  by auto
   1.115  
   1.116  lemma DEF_INTER:
   1.117    "op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
   1.118 -  by (auto simp add: mem_def fun_eq_iff Collect_def)
   1.119 +  by auto
   1.120  
   1.121  lemma DEF_INSERT:
   1.122    "insert = (%u ua y. y \<in> ua | y = u)"
   1.123 @@ -202,10 +199,6 @@
   1.124    "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
   1.125    by (simp add: fun_eq_iff image_def Bex_def)
   1.126  
   1.127 -lemma DEF_GSPEC:
   1.128 -  "Collect = (\<lambda>u. u)"
   1.129 -  by (simp add: Collect_def ext)
   1.130 -
   1.131  lemma DEF_GEQ:
   1.132    "(op =) = (op =)"
   1.133    by simp
   1.134 @@ -226,9 +219,7 @@
   1.135    apply (erule finite_induct)
   1.136    apply auto[2]
   1.137    apply (drule_tac x="finite" in spec)
   1.138 -  apply auto
   1.139 -  apply (metis Collect_def Collect_empty_eq finite.emptyI)
   1.140 -  by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
   1.141 +  by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
   1.142  
   1.143  lemma DEF_FACT:
   1.144    "fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
   1.145 @@ -260,10 +251,9 @@
   1.146    apply simp_all
   1.147    done
   1.148  
   1.149 -lemma DEF_EMPTY: "{} = (%x. False)"
   1.150 -  unfolding fun_eq_iff empty_def
   1.151 -  by auto
   1.152 -
   1.153 +lemma DEF_EMPTY: "bot = (%x. False)"
   1.154 +  by (rule ext) auto
   1.155 +  
   1.156  lemma DEF_DIV:
   1.157    "op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
   1.158       else m = q m n * n + r m n \<and> r m n < n)"
   1.159 @@ -286,8 +276,7 @@
   1.160  
   1.161  lemma DEF_DIFF:
   1.162    "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
   1.163 -  by (simp add: fun_eq_iff Collect_def)
   1.164 -     (metis DiffE DiffI mem_def)
   1.165 +  by (metis set_diff_eq)
   1.166  
   1.167  definition [hol4rew]: "DELETE s e = s - {e}"
   1.168  
   1.169 @@ -345,11 +334,8 @@
   1.170  lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
   1.171    by (simp add: mem_def)
   1.172  
   1.173 -definition dotdot :: "nat => nat => nat => bool"
   1.174 -  where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
   1.175 -
   1.176 -lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
   1.177 -  by (simp add: dotdot_def)
   1.178 +definition dotdot :: "nat => nat => nat set"
   1.179 +  where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
   1.180  
   1.181  lemma [hol4rew]: "dotdot a b = {a..b}"
   1.182    unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def